let n, k be Nat; :: thesis: for i1 being Element of n holds i1 is Element of n + k
let i1 be Element of n; :: thesis: i1 is Element of n + k
i1 is Element of Segm n ;
then reconsider I = i1 as Nat ;

per cases ( ( n = 0 & k = 0 ) or ( n = 0 & k > 0 ) or n <> 0 ) ;

suppose ( n = 0 & k = 0 ) ; :: thesis: i1 is Element of n + k

hence i1 is Element of n + k ; :: thesis: verum

end;

suppose A1: ( n = 0 & k > 0 ) ; :: thesis: i1 is Element of n + k

then i1 is empty by SUBSET_1:def 1;
then I in Segm (n + k) by A1, NAT_1:44;
hence i1 is Element of n + k ; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: i1 is Element of n + k

then I in Segm n ;
then ( I < n & n <= n + k ) by NAT_1:11, NAT_1:44;
then I < n + k by XXREAL_0:2;
then I in Segm (n + k) by NAT_1:44;
hence i1 is Element of n + k ; :: thesis: verum

end;

end;