let M be non empty set ; :: thesis: for T being non empty TopSpace holds RelStr(# the carrier of (Omega (product (M --> T))), the InternalRel of (Omega (product (M --> T))) #) = RelStr(# the carrier of (product (M --> (Omega T))), the InternalRel of (product (M --> (Omega T))) #)
let T be non empty TopSpace; :: thesis: RelStr(# the carrier of (Omega (product (M --> T))), the InternalRel of (Omega (product (M --> T))) #) = RelStr(# the carrier of (product (M --> (Omega T))), the InternalRel of (product (M --> (Omega T))) #)
A1: dom (Carrier (M --> T)) = M by PARTFUN1:def 2
.= dom (Carrier (M --> (Omega T))) by PARTFUN1:def 2 ;
A2: for i being object st i in dom (Carrier (M --> T)) holds
(Carrier (M --> T)) . i = (Carrier (M --> (Omega T))) . i
proof
let i be object ; :: thesis: ( i in dom (Carrier (M --> T)) implies (Carrier (M --> T)) . i = (Carrier (M --> (Omega T))) . i )
assume i in dom (Carrier (M --> T)) ; :: thesis: (Carrier (M --> T)) . i = (Carrier (M --> (Omega T))) . i
then A3: i in M ;
then consider R1 being 1-sorted such that
A4: R1 = (M --> T) . i and
A5: (Carrier (M --> T)) . i = the carrier of R1 by PRALG_1:def 15;
consider R2 being 1-sorted such that
A6: R2 = (M --> (Omega T)) . i and
A7: (Carrier (M --> (Omega T))) . i = the carrier of R2 by A3, PRALG_1:def 15;
the carrier of R1 = the carrier of T by A3, A4, FUNCOP_1:7
.= the carrier of (Omega T) by Lm1
.= the carrier of R2 by A3, A6, FUNCOP_1:7 ;
hence (Carrier (M --> T)) . i = (Carrier (M --> (Omega T))) . i by A5, A7; :: thesis: verum
end;
A8: the carrier of (Omega (product (M --> T))) = the carrier of (product (M --> T)) by Lm1
.= product (Carrier (M --> T)) by WAYBEL18:def 3
.= product (Carrier (M --> (Omega T))) by A1, A2, FUNCT_1:2 ;
A9: the carrier of (Omega (product (M --> T))) = the carrier of (product (M --> T)) by Lm1;
the InternalRel of (Omega (product (M --> T))) = the InternalRel of (product (M --> (Omega T)))
proof
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in the InternalRel of (Omega (product (M --> T))) or [x,y] in the InternalRel of (product (M --> (Omega T))) ) & ( not [x,y] in the InternalRel of (product (M --> (Omega T))) or [x,y] in the InternalRel of (Omega (product (M --> T))) ) )
hereby :: thesis: ( not [x,y] in the InternalRel of (product (M --> (Omega T))) or [x,y] in the InternalRel of (Omega (product (M --> T))) )
assume A10: [x,y] in the InternalRel of (Omega (product (M --> T))) ; :: thesis: [x,y] in the InternalRel of (product (M --> (Omega T)))
then A11: y in the carrier of (Omega (product (M --> T))) by ZFMISC_1:87;
A12: x in the carrier of (Omega (product (M --> T))) by A10, ZFMISC_1:87;
then reconsider xp = x, yp = y as Element of (product (M --> (Omega T))) by A8, A11, YELLOW_1:def 4;
reconsider p1 = x, p2 = y as Element of (product (M --> T)) by A12, A11, Lm1;
reconsider xo = x, yo = y as Element of (Omega (product (M --> T))) by A10, ZFMISC_1:87;
A13: xp in product (Carrier (M --> (Omega T))) by A8, A10, ZFMISC_1:87;
then consider f being Function such that
A14: xp = f and
dom f = dom (Carrier (M --> (Omega T))) and
for i being object st i in dom (Carrier (M --> (Omega T))) holds
f . i in (Carrier (M --> (Omega T))) . i by CARD_3:def 5;
yp in product (Carrier (M --> (Omega T))) by A8, A10, ZFMISC_1:87;
then consider g being Function such that
A15: yp = g and
dom g = dom (Carrier (M --> (Omega T))) and
for i being object st i in dom (Carrier (M --> (Omega T))) holds
g . i in (Carrier (M --> (Omega T))) . i by CARD_3:def 5;
xo <= yo by A10;
then A16: ex Yp being Subset of (product (M --> T)) st
( Yp = {p2} & p1 in Cl Yp ) by Def2;
for i being object st i in M holds
ex R being RelStr ex xi, yi being Element of R st
( R = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi )
proof
let i be object ; :: thesis: ( i in M implies ex R being RelStr ex xi, yi being Element of R st
( R = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi ) )
assume A17: i in M ; :: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi )
then reconsider j = i as Element of M ;
set t1 = p1 . j;
set t2 = p2 . j;
reconsider xi = p1 . j, yi = p2 . j as Element of (Omega T) by Lm1;
take Omega T ; :: thesis: ex xi, yi being Element of (Omega T) st
( Omega T = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi )
take xi ; :: thesis: ex yi being Element of (Omega T) st
( Omega T = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi )
take yi ; :: thesis: ( Omega T = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi )
thus Omega T = (M --> (Omega T)) . i by A17, FUNCOP_1:7; :: thesis: ( xi = f . i & yi = g . i & xi <= yi )
thus xi = f . i by A14; :: thesis: ( yi = g . i & xi <= yi )
thus yi = g . i by A15; :: thesis: xi <= yi
p1 . j in Cl {(p2 . j)} by A16, YELLOW14:30;
hence xi <= yi by Def2; :: thesis: verum
end;
then xp <= yp by A13, A14, A15, YELLOW_1:def 4;
hence [x,y] in the InternalRel of (product (M --> (Omega T))) ; :: thesis: verum
end;
assume A18: [x,y] in the InternalRel of (product (M --> (Omega T))) ; :: thesis: [x,y] in the InternalRel of (Omega (product (M --> T)))
then reconsider xp = x, yp = y as Element of (product (M --> (Omega T))) by ZFMISC_1:87;
A19: xp <= yp by A18;
A20: x in the carrier of (product (M --> (Omega T))) by A18, ZFMISC_1:87;
then xp in product (Carrier (M --> (Omega T))) by YELLOW_1:def 4;
then consider f, g being Function such that
A21: f = xp and
A22: g = yp and
A23: for i being object st i in M holds
ex R being RelStr ex xi, yi being Element of R st
( R = (M --> (Omega T)) . i & xi = f . i & yi = g . i & xi <= yi ) by A19, YELLOW_1:def 4;
A24: y in the carrier of (product (M --> (Omega T))) by A18, ZFMISC_1:87;
then reconsider xo = x, yo = y as Element of (Omega (product (M --> T))) by A8, A20, YELLOW_1:def 4;
reconsider p1 = x, p2 = y as Element of (product (M --> T)) by A8, A9, A20, A24, YELLOW_1:def 4;
for i being Element of M holds p1 . i in Cl {(p2 . i)}
proof
let i be Element of M; :: thesis: p1 . i in Cl {(p2 . i)}
consider R1 being RelStr , xi, yi being Element of R1 such that
A25: R1 = (M --> (Omega T)) . i and
A26: xi = f . i and
A27: yi = g . i and
A28: xi <= yi by A23;
reconsider xi = xi, yi = yi as Element of (Omega T) by A25;
xi <= yi by A25, A28;
then ex Y being Subset of T st
( Y = {yi} & xi in Cl Y ) by Def2;
hence p1 . i in Cl {(p2 . i)} by A21, A22, A26, A27; :: thesis: verum
end;
then p1 in Cl {p2} by YELLOW14:30;
then xo <= yo by Def2;
hence [x,y] in the InternalRel of (Omega (product (M --> T))) ; :: thesis: verum
end;
hence RelStr(# the carrier of (Omega (product (M --> T))), the InternalRel of (Omega (product (M --> T))) #) = RelStr(# the carrier of (product (M --> (Omega T))), the InternalRel of (product (M --> (Omega T))) #) by A8, YELLOW_1:def 4; :: thesis: verum