defpred S₁[ set , set ] means for i, j being Element of NAT st $1 = [i,j] holds
$2 = [:(Im (Nbdl1 n),i),(Im (Nbdl1 m),j):];
A1: for x being set st x in [:(Seg n),(Seg m):] holds
ex y being set st
( y in bool [:(Seg n),(Seg m):] & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in [:(Seg n),(Seg m):] implies ex y being set st
( y in bool [:(Seg n),(Seg m):] & S₁[x,y] ) )
assume x in [:(Seg n),(Seg m):] ; :: thesis: ex y being set st
( y in bool [:(Seg n),(Seg m):] & S₁[x,y] )
then consider u, y being set such that
A2: ( u in Seg n & y in Seg m ) and
A3: x = [u,y] by ZFMISC_1:def 2;
reconsider i = u, j = y as Element of NAT by A2;
set y3 = [:(Im (Nbdl1 n),i),(Im (Nbdl1 m),j):];
A4: [:(Im (Nbdl1 n),i),(Im (Nbdl1 m),j):] c= [:(Seg n),(Seg m):]

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in [:(Im (Nbdl1 n),i),(Im (Nbdl1 m),j):] or z in [:(Seg n),(Seg m):] )
assume z in [:(Im (Nbdl1 n),i),(Im (Nbdl1 m),j):] ; :: thesis: z in [:(Seg n),(Seg m):]
then ex x4, y4 being set st
( x4 in Im (Nbdl1 n),i & y4 in Im (Nbdl1 m),j & z = [x4,y4] ) by ZFMISC_1:def 2;
hence z in [:(Seg n),(Seg m):] by ZFMISC_1:def 2; :: thesis: verum

end;

for i4, j4 being Element of NAT st x = [i4,j4] holds
[:(Im (Nbdl1 n),i),(Im (Nbdl1 m),j):] = [:(Im (Nbdl1 n),i4),(Im (Nbdl1 m),j4):]

proof

let i4, j4 be Element of NAT ; :: thesis: ( x = [i4,j4] implies [:(Im (Nbdl1 n),i),(Im (Nbdl1 m),j):] = [:(Im (Nbdl1 n),i4),(Im (Nbdl1 m),j4):] )
assume A5: x = [i4,j4] ; :: thesis: [:(Im (Nbdl1 n),i),(Im (Nbdl1 m),j):] = [:(Im (Nbdl1 n),i4),(Im (Nbdl1 m),j4):]
then i4 = u by A3, ZFMISC_1:33;
hence [:(Im (Nbdl1 n),i),(Im (Nbdl1 m),j):] = [:(Im (Nbdl1 n),i4),(Im (Nbdl1 m),j4):] by A3, A5, ZFMISC_1:33; :: thesis: verum

end;

hence ex y being set st
( y in bool [:(Seg n),(Seg m):] & S₁[x,y] ) by A4; :: thesis: verum

end;

consider f being Function of [:(Seg n),(Seg m):],(bool [:(Seg n),(Seg m):]) such that
A6: for x being set st x in [:(Seg n),(Seg m):] holds
S₁[x,f . x] from FUNCT_2:sch 1(A1);
consider R being Relation of [:(Seg n),(Seg m):] such that
A7: for i being set st i in [:(Seg n),(Seg m):] holds
Im R,i = f . i by FUNCT_2:170;
take R ; :: thesis: for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im R,x = [:(Im (Nbdl1 n),i),(Im (Nbdl1 m),j):]
let x be set ; :: thesis: ( x in [:(Seg n),(Seg m):] implies for i, j being Element of NAT st x = [i,j] holds
Im R,x = [:(Im (Nbdl1 n),i),(Im (Nbdl1 m),j):] )
assume A8: x in [:(Seg n),(Seg m):] ; :: thesis: for i, j being Element of NAT st x = [i,j] holds
Im R,x = [:(Im (Nbdl1 n),i),(Im (Nbdl1 m),j):]
let i, j be Element of NAT ; :: thesis: ( x = [i,j] implies Im R,x = [:(Im (Nbdl1 n),i),(Im (Nbdl1 m),j):] )
assume A9: x = [i,j] ; :: thesis: Im R,x = [:(Im (Nbdl1 n),i),(Im (Nbdl1 m),j):]
thus Im R,x = f . x by A7, A8
.= [:(Im (Nbdl1 n),i),(Im (Nbdl1 m),j):] by A6, A8, A9 ; :: thesis: verum