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;

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

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;

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