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;
hence ( [(i + k),j] in square-uparrow n & [i,(j + l)] in square-uparrow n ) ; :: thesis: verum