I heard about the modal logic K, but I am not sure about NK -- what additional axioms it has.

I don't understand how line 4 was obtained. I guess, one has to prove □p \/ □q -> □(p \/ q). For this, one proves □p -> □(p \/ q) and □q -> □(p \/ q). This follows from p -> p \/ q, q -> p \/ q and the Nec rule and distributivity.

I also don't see how to get line 6 -- this is at least not a one-step transition.