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

proof

let x be object ; :: thesis: ( x in [:(Seg n),(Seg m):] implies ex y being object st
( y in bool [:(Seg n),(Seg m):] & S₁[x,y] ) )
assume x in [:(Seg n),(Seg m):] ; :: thesis: ex y being object st
( y in bool [:(Seg n),(Seg m):] & S₁[x,y] )
then consider u, y being object 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 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 object ; :: 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 object 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 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 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, XTUPLE_0:1;
hence [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] = [:(Im ((Nbdl1 n),i4)),(Im ((Nbdl1 m),j4)):] by A3, A5, XTUPLE_0:1; :: thesis: verum

end;

hence ex y being object 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 object 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:93;
take R ; :: thesis: for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being 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 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 Nat st x = [i,j] holds
Im (R,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):]
let i, j be 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