defpred S_{1}[ 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_{1}[x,y] )

A6: for x being object st x in [:(Seg n),(Seg m):] holds

S_{1}[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

$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

proof

consider f being Function of [:(Seg n),(Seg m):],(bool [:(Seg n),(Seg m):]) such that
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_{1}[x,y] ) )

assume x in [:(Seg n),(Seg m):] ; :: thesis: ex y being object st

( y in bool [:(Seg n),(Seg m):] & S_{1}[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):]

[:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] = [:(Im ((Nbdl1 n),i4)),(Im ((Nbdl1 m),j4)):]

( y in bool [:(Seg n),(Seg m):] & S_{1}[x,y] )
by A4; :: thesis: verum

end;( y in bool [:(Seg n),(Seg m):] & S

assume x in [:(Seg n),(Seg m):] ; :: thesis: ex y being object st

( y in bool [:(Seg n),(Seg m):] & S

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

for i4, j4 being Nat st x = [i4,j4] holds
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;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

[:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] = [:(Im ((Nbdl1 n),i4)),(Im ((Nbdl1 m),j4)):]

proof

hence
ex y being object st
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;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

( y in bool [:(Seg n),(Seg m):] & S

A6: for x being object st x in [:(Seg n),(Seg m):] holds

S

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