let i, j, k, l, n be Nat; :: thesis: ( [i,j] in square-uparrow n implies ( [(i + k),j] in square-uparrow n & [i,(j + l)] in square-uparrow n ) )

assume [i,j] in square-uparrow n ; :: thesis: ( [(i + k),j] in square-uparrow n & [i,(j + l)] in square-uparrow n )

then consider i1, j1 being Nat such that

A1: i1 = [i,j] `1 and

A2: j1 = [i,j] `2 and

A3: n <= i1 and

A4: n <= j1 by Def3;

( i <= i + k & j <= j + l ) by NAT_1:11;

then A5: ( n <= i + k & n <= j + l ) by A1, A2, A3, A4, XXREAL_0:2;

( i in NAT & i + k in NAT & j in NAT & j + l in NAT ) by ORDINAL1:def 12;

then reconsider x = [(i + k),j], y = [i,(j + l)] as Element of [:NAT,NAT:] by ZFMISC_1:def 2;

assume [i,j] in square-uparrow n ; :: thesis: ( [(i + k),j] in square-uparrow n & [i,(j + l)] in square-uparrow n )

then consider i1, j1 being Nat such that

A1: i1 = [i,j] `1 and

A2: j1 = [i,j] `2 and

A3: n <= i1 and

A4: n <= j1 by Def3;

( i <= i + k & j <= j + l ) by NAT_1:11;

then A5: ( n <= i + k & n <= j + l ) by A1, A2, A3, A4, XXREAL_0:2;

( i in NAT & i + k in NAT & j in NAT & j + l in NAT ) by ORDINAL1:def 12;

then reconsider x = [(i + k),j], y = [i,(j + l)] as Element of [:NAT,NAT:] by ZFMISC_1:def 2;

now :: thesis: ( x in square-uparrow n & y in square-uparrow n )

hence
( [(i + k),j] in square-uparrow n & [i,(j + l)] in square-uparrow n )
; :: thesis: verum
ex i2, j1 being Nat st

( i2 = x `1 & j1 = x `2 & n <= i + k & n <= j ) by A2, A4, A5;

hence x in square-uparrow n by Def3; :: thesis: y in square-uparrow n

ex i1, j2 being Nat st

( i1 = y `1 & j2 = y `2 & n <= i & n <= j + l ) by A1, A3, A5;

hence y in square-uparrow n by Def3; :: thesis: verum

end;( i2 = x `1 & j1 = x `2 & n <= i + k & n <= j ) by A2, A4, A5;

hence x in square-uparrow n by Def3; :: thesis: y in square-uparrow n

ex i1, j2 being Nat st

( i1 = y `1 & j2 = y `2 & n <= i & n <= j + l ) by A1, A3, A5;

hence y in square-uparrow n by Def3; :: thesis: verum