per cases ( k = - 1 or k is natural ) by Def11;

suppose A1: k = - 1 ; :: thesis: k + n is natural

consider i being Nat such that
A2: n = i + 1 by NAT_1:6;
k + n = i by A2, A1;
hence k + n is natural ; :: thesis: verum

end;

suppose k is natural ; :: thesis: k + n is natural

hence k + n is natural ; :: thesis: verum

end;

end;