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 ;

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 )
;

end;