defpred S1[ 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):] & S1[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):] & S1[x,y] ) )
assume x in [:(Seg n),(Seg m):] ; :: thesis: ex y being object st
( y in bool [:(Seg n),(Seg m):] & S1[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):]
proof
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):]
per cases ( z in [:{i},(Im ((Nbdl1 m),j)):] or z in [:(Im ((Nbdl1 n),u)),{j}:] ) by A6, XBOOLE_0:def 3;
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;
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;
end;
end;
for i4, j4 being Nat st x = [i4,j4] holds
[:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] = [:{i4},(Im ((Nbdl1 m),j4)):] \/ [:(Im ((Nbdl1 n),i4)),{j4}:]
proof
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;
hence ex y being object st
( y in bool [:(Seg n),(Seg m):] & S1[x,y] ) by A5; :: thesis: verum
end;
consider f being Function of [:(Seg n),(Seg m):],(bool [:(Seg n),(Seg m):]) such that
A12: for x being object st x in [:(Seg n),(Seg m):] holds
S1[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