let i, j, k, l, n be Nat; ( [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
; ( [(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 )
; verum