defpred S1[ 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):] & S1[x,y] )
proof
let x be
object ;
( 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):]
;
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 &
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 ;
TARSKI:def 3 ( 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)):]
;
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;
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;
( 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]
;
[:(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;
verum
end;
hence
ex
y being
object st
(
y in bool [:(Seg n),(Seg m):] &
S1[
x,
y] )
by A4;
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
S1[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
; 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 ; ( 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):]
; 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; ( x = [i,j] implies Im (R,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] )
assume A9:
x = [i,j]
; 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
; verum