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 4
.= dom (Carrier (M --> (Omega T))) by PARTFUN1:def 4 ;
A2: for i being set st i in dom (Carrier (M --> T)) holds
(Carrier (M --> T)) . i = (Carrier (M --> (Omega T))) . i

proof

let i be set ; :: 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 by PARTFUN1:def 4;
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 13;
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 13;
the carrier of R1 = the carrier of T by A3, A4, FUNCOP_1:13
.= the carrier of (Omega T) by Lm1
.= the carrier of R2 by A3, A6, FUNCOP_1:13 ;
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:9 ;
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 set ; :: 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: ( x in the carrier of (Omega (product (M --> T))) & y in the carrier of (Omega (product (M --> T))) ) by ZFMISC_1:106;
reconsider xo = x, yo = y as Element of (Omega (product (M --> T))) by A10, ZFMISC_1:106;
reconsider p1 = x, p2 = y as Element of (product (M --> T)) by A11, Lm1;
reconsider xp = x, yp = y as Element of (product (M --> (Omega T))) by A8, A11, YELLOW_1:def 4;
xo <= yo by A10, ORDERS_2:def 9;
then consider Yp being Subset of (product (M --> T)) such that
A12: Yp = {p2} and
A13: p1 in Cl Yp by Def2;
A14: xp in product (Carrier (M --> (Omega T))) by A8, A10, ZFMISC_1:106;
then consider f being Function such that
A15: xp = f and
dom f = dom (Carrier (M --> (Omega T))) and
for i being set 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:106;
then consider g being Function such that
A16: yp = g and
dom g = dom (Carrier (M --> (Omega T))) and
for i being set st i in dom (Carrier (M --> (Omega T))) holds
g . i in (Carrier (M --> (Omega T))) . i by CARD_3:def 5;
for i being set 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 set ; :: 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 ;
A18: p1 . j in Cl {(p2 . j)} by A12, A13, YELLOW14:31;
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:13; :: thesis: ( xi = f . i & yi = g . i & xi <= yi )
thus xi = f . i by A15; :: thesis: ( yi = g . i & xi <= yi )
thus yi = g . i by A16; :: thesis: xi <= yi
thus xi <= yi by A18, Def2; :: thesis: verum

end;

then xp <= yp by A14, A15, A16, YELLOW_1:def 4;
hence [x,y] in the InternalRel of (product (M --> (Omega T))) by ORDERS_2:def 9; :: thesis: verum

end;

assume A19: [x,y] in the InternalRel of (product (M --> (Omega T))) ; :: thesis: [x,y] in the InternalRel of (Omega (product (M --> T)))
then A20: ( x in the carrier of (product (M --> (Omega T))) & y in the carrier of (product (M --> (Omega T))) ) by ZFMISC_1:106;
reconsider xp = x, yp = y as Element of (product (M --> (Omega T))) by A19, ZFMISC_1:106;
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, YELLOW_1:def 4;
A21: xp in product (Carrier (M --> (Omega T))) by A20, YELLOW_1:def 4;
xp <= yp by A19, ORDERS_2:def 9;
then consider f, g being Function such that
A22: f = xp and
A23: g = yp and
A24: for i being set 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 A21, 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 & yi = g . i ) and
A27: xi <= yi by A24;
reconsider xi = xi, yi = yi as Element of (Omega T) by A25, FUNCOP_1:13;
xi <= yi by A25, A27, FUNCOP_1:13;
then ex Y being Subset of T st
( Y = {yi} & xi in Cl Y ) by Def2;
hence p1 . i in Cl {(p2 . i)} by A22, A23, A26; :: thesis: verum

end;

then p1 in Cl {p2} by YELLOW14:31;
then xo <= yo by Def2;
hence [x,y] in the InternalRel of (Omega (product (M --> T))) by ORDERS_2:def 9; :: 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