defpred S_{1}[ object , object ] means for i, j being Nat st $1 = [i,j] holds

$2 = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{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] )

A12: 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

A13: 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) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{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) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] )

assume A14: x in [:(Seg n),(Seg m):] ; :: thesis: for i, j being Nat st x = [i,j] holds

Im (R,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:]

let i, j be Nat; :: thesis: ( x = [i,j] implies Im (R,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] )

assume A15: x = [i,j] ; :: thesis: Im (R,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:]

thus Im (R,x) = f . x by A13, A14

.= [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] by A12, A14, A15 ; :: thesis: verum

$2 = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{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 and

A3: y in Seg m and

A4: x = [u,y] by ZFMISC_1:def 2;

reconsider i = u, j = y as Nat by A2, A3;

set y3 = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:];

A5: [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] c= [:(Seg n),(Seg m):]

[:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] = [:{i4},(Im ((Nbdl1 m),j4)):] \/ [:(Im ((Nbdl1 n),i4)),{j4}:]

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

A3: y in Seg m and

A4: x = [u,y] by ZFMISC_1:def 2;

reconsider i = u, j = y as Nat by A2, A3;

set y3 = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:];

A5: [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{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 [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] or z in [:(Seg n),(Seg m):] )

assume A6: z in [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] ; :: thesis: z in [:(Seg n),(Seg m):]

end;assume A6: z in [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] ; :: thesis: z in [:(Seg n),(Seg m):]

per cases
( z in [:{i},(Im ((Nbdl1 m),j)):] or z in [:(Im ((Nbdl1 n),u)),{j}:] )
by A6, XBOOLE_0:def 3;

end;

suppose
z in [:{i},(Im ((Nbdl1 m),j)):]
; :: thesis: z in [:(Seg n),(Seg m):]

then consider x4, y4 being object such that

A7: x4 in {i} and

A8: ( y4 in Im ((Nbdl1 m),j) & z = [x4,y4] ) by ZFMISC_1:def 2;

x4 = i by A7, TARSKI:def 1;

hence z in [:(Seg n),(Seg m):] by A2, A8, ZFMISC_1:def 2; :: thesis: verum

end;A7: x4 in {i} and

A8: ( y4 in Im ((Nbdl1 m),j) & z = [x4,y4] ) by ZFMISC_1:def 2;

x4 = i by A7, TARSKI:def 1;

hence z in [:(Seg n),(Seg m):] by A2, A8, ZFMISC_1:def 2; :: thesis: verum

suppose
z in [:(Im ((Nbdl1 n),u)),{j}:]
; :: thesis: z in [:(Seg n),(Seg m):]

then consider x4, y4 being object such that

A9: x4 in Im ((Nbdl1 n),i) and

A10: y4 in {j} and

A11: z = [x4,y4] by ZFMISC_1:def 2;

y4 in Seg m by A3, A10, TARSKI:def 1;

hence z in [:(Seg n),(Seg m):] by A9, A11, ZFMISC_1:def 2; :: thesis: verum

end;A9: x4 in Im ((Nbdl1 n),i) and

A10: y4 in {j} and

A11: z = [x4,y4] by ZFMISC_1:def 2;

y4 in Seg m by A3, A10, TARSKI:def 1;

hence z in [:(Seg n),(Seg m):] by A9, A11, ZFMISC_1:def 2; :: thesis: verum

[:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] = [:{i4},(Im ((Nbdl1 m),j4)):] \/ [:(Im ((Nbdl1 n),i4)),{j4}:]

proof

hence
ex y being object st
let i4, j4 be Nat; :: thesis: ( x = [i4,j4] implies [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] = [:{i4},(Im ((Nbdl1 m),j4)):] \/ [:(Im ((Nbdl1 n),i4)),{j4}:] )

assume x = [i4,j4] ; :: thesis: [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] = [:{i4},(Im ((Nbdl1 m),j4)):] \/ [:(Im ((Nbdl1 n),i4)),{j4}:]

then ( i4 = u & j4 = y ) by A4, XTUPLE_0:1;

hence [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] = [:{i4},(Im ((Nbdl1 m),j4)):] \/ [:(Im ((Nbdl1 n),i4)),{j4}:] ; :: thesis: verum

end;assume x = [i4,j4] ; :: thesis: [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] = [:{i4},(Im ((Nbdl1 m),j4)):] \/ [:(Im ((Nbdl1 n),i4)),{j4}:]

then ( i4 = u & j4 = y ) by A4, XTUPLE_0:1;

hence [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] = [:{i4},(Im ((Nbdl1 m),j4)):] \/ [:(Im ((Nbdl1 n),i4)),{j4}:] ; :: thesis: verum

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

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

S

consider R being Relation of [:(Seg n),(Seg m):] such that

A13: 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) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{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) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] )

assume A14: x in [:(Seg n),(Seg m):] ; :: thesis: for i, j being Nat st x = [i,j] holds

Im (R,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:]

let i, j be Nat; :: thesis: ( x = [i,j] implies Im (R,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] )

assume A15: x = [i,j] ; :: thesis: Im (R,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:]

thus Im (R,x) = f . x by A13, A14

.= [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] by A12, A14, A15 ; :: thesis: verum