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;