let X be non empty TopSpace; :: thesis: for M being non empty set ex F being Function of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))),(M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) st
( F is isomorphic & ( for f being continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)) holds F . f = commute f ) )
let M be non empty set ; :: thesis: ex F being Function of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))),(M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) st
( F is isomorphic & ( for f being continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)) holds F . f = commute f ) )
set S = Sierpinski_Space ;
set S9M = M -TOP_prod (M --> Sierpinski_Space);
set XxxS9M = oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)));
set XxS = oContMaps (X,Sierpinski_Space);
set XxS9xM = M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)));
deffunc H₁( Element of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))))) -> set = commute $1;
consider F being ManySortedSet of the carrier of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) such that
A1: for f being Element of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) holds F . f = H₁(f) from PBOOLE:sch 5();
A2: dom F = the carrier of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) by PARTFUN1:def 2;
rng F c= the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))))

proof

let g be object ; :: according to TARSKI:def 3 :: thesis: ( not g in rng F or g in the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) )
assume g in rng F ; :: thesis: g in the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))))
then consider f being object such that
A3: f in dom F and
A4: g = F . f by FUNCT_1:def 3;
reconsider f = f as continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)) by A3, Th2;
g = commute f by A1, A3, A4;
then reconsider g = g as Function of M, the carrier of (oContMaps (X,Sierpinski_Space)) by Th31;
( dom g = M & rng g c= the carrier of (oContMaps (X,Sierpinski_Space)) ) by FUNCT_2:def 1;
then g in Funcs (M, the carrier of (oContMaps (X,Sierpinski_Space))) by FUNCT_2:def 2;
then g in the carrier of ((oContMaps (X,Sierpinski_Space)) |^ M) by YELLOW_1:28;
hence g in the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) by YELLOW_1:def 5; :: thesis: verum

end;

then reconsider F = F as Function of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))),(M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) by A2, FUNCT_2:2;
deffunc H₂( Element of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))))) -> set = commute $1;
consider G being ManySortedSet of the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) such that
A5: for f being Element of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) holds G . f = H₂(f) from PBOOLE:sch 5();
A6: dom G = the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) by PARTFUN1:def 2;
A7: rng G c= the carrier of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))))

proof

let g be object ; :: according to TARSKI:def 3 :: thesis: ( not g in rng G or g in the carrier of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) )
assume g in rng G ; :: thesis: g in the carrier of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))))
then consider f being object such that
A8: f in dom G and
A9: g = G . f by FUNCT_1:def 3;
f in the carrier of ((oContMaps (X,Sierpinski_Space)) |^ M) by A6, A8, YELLOW_1:def 5;
then f in Funcs (M, the carrier of (oContMaps (X,Sierpinski_Space))) by YELLOW_1:28;
then consider f9 being Function such that
A10: f = f9 and
A11: ( dom f9 = M & rng f9 c= the carrier of (oContMaps (X,Sierpinski_Space)) ) by FUNCT_2:def 2;
A12: f9 is Function of M, the carrier of (oContMaps (X,Sierpinski_Space)) by A11, FUNCT_2:2;
g = commute f9 by A5, A8, A9, A10;
then g is continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)) by A12, Th33;
then g is Element of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) by Th2;
hence g in the carrier of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) ; :: thesis: verum

end;

take F ; :: thesis: ( F is isomorphic & ( for f being continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)) holds F . f = commute f ) )
A13: the carrier of (M -TOP_prod (M --> Sierpinski_Space)) = product (Carrier (M --> Sierpinski_Space)) by WAYBEL18:def 3
.= product (M --> the carrier of Sierpinski_Space) by Th30
.= Funcs (M, the carrier of Sierpinski_Space) by CARD_3:11 ;
reconsider G = G as Function of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))),(oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) by A6, A7, FUNCT_2:2;
A14: the carrier of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) c= Funcs ( the carrier of X, the carrier of (M -TOP_prod (M --> Sierpinski_Space))) by Th32;

now :: thesis: for a being Element of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) holds (G * F) . a = (id (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))))) . a

let a be Element of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))); :: thesis: (G * F) . a = (id (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))))) . a
A15: commute (commute a) = a by A14, A13, FUNCT_6:57;
thus (G * F) . a = G . (F . a) by FUNCT_2:15
.= commute (F . a) by A5
.= a by A1, A15
.= (id (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))))) . a ; :: thesis: verum

end;

then A16: G * F = id (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) by FUNCT_2:63;
A17: RelStr(# the carrier of (Omega (M -TOP_prod (M --> Sierpinski_Space))), the InternalRel of (Omega (M -TOP_prod (M --> Sierpinski_Space))) #) = M -POS_prod (M --> (Omega Sierpinski_Space)) by WAYBEL25:14;
A18: F is monotone

proof

let a, b be Element of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))); :: according to WAYBEL_1:def 2 :: thesis: ( not a <= b or F . a <= F . b )
assume A19: a <= b ; :: thesis: F . a <= F . b
reconsider f9 = a, g9 = b as continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)) by Th2;
reconsider f = a, g = b as continuous Function of X,(Omega (M -TOP_prod (M --> Sierpinski_Space))) by Th1;

now :: thesis: for i being Element of M holds (F . a) . i <= (F . b) . i

let i be Element of M; :: thesis: (F . a) . i <= (F . b) . i
A20: (M --> (oContMaps (X,Sierpinski_Space))) . i = oContMaps (X,Sierpinski_Space) by FUNCOP_1:7;
then reconsider Fai = (F . a) . i, Fbi = (F . b) . i as continuous Function of X,(Omega Sierpinski_Space) by Th1;

now :: thesis: for j being set st j in the carrier of X holds
ex a, b being Element of (Omega Sierpinski_Space) st
( a = Fai . j & b = Fbi . j & a <= b )

let j be set ; :: thesis: ( j in the carrier of X implies ex a, b being Element of (Omega Sierpinski_Space) st
( a = Fai . j & b = Fbi . j & a <= b ) )
assume j in the carrier of X ; :: thesis: ex a, b being Element of (Omega Sierpinski_Space) st
( a = Fai . j & b = Fbi . j & a <= b )
then reconsider x = j as Element of X ;
( b in the carrier of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) & F . b = commute g ) by A1;
then A21: Fbi . x = (g9 . x) . i by A14, A13, FUNCT_6:56;
reconsider fx = f . x, gx = g . x as Element of (M -POS_prod (M --> (Omega Sierpinski_Space))) by A17;
( a in the carrier of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) & F . a = commute f ) by A1;
then A22: Fai . x = (f9 . x) . i by A14, A13, FUNCT_6:56;
f <= g by A19, Th3;
then ex a, b being Element of (Omega (M -TOP_prod (M --> Sierpinski_Space))) st
( a = f . x & b = g . x & a <= b ) ;
then fx <= gx by A17, YELLOW_0:1;
then A23: fx . i <= gx . i by WAYBEL_3:28;
(M --> (Omega Sierpinski_Space)) . i = Omega Sierpinski_Space by FUNCOP_1:7;
hence ex a, b being Element of (Omega Sierpinski_Space) st
( a = Fai . j & b = Fbi . j & a <= b ) by A22, A21, A23; :: thesis: verum

end;

then Fai <= Fbi ;
hence (F . a) . i <= (F . b) . i by A20, Th3; :: thesis: verum

end;

hence F . a <= F . b by WAYBEL_3:28; :: thesis: verum

end;

A24: the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) = the carrier of ((oContMaps (X,Sierpinski_Space)) |^ M) by YELLOW_1:def 5
.= Funcs (M, the carrier of (oContMaps (X,Sierpinski_Space))) by YELLOW_1:28 ;
then A25: the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) c= Funcs (M,(Funcs ( the carrier of X, the carrier of Sierpinski_Space))) by Th32, FUNCT_5:56;
A26: G is monotone

proof

let a, b be Element of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))); :: according to WAYBEL_1:def 2 :: thesis: ( not a <= b or G . a <= G . b )
assume A27: a <= b ; :: thesis: G . a <= G . b
reconsider f = G . a, g = G . b as continuous Function of X,(Omega (M -TOP_prod (M --> Sierpinski_Space))) by Th1;

now :: thesis: for i being set st i in the carrier of X holds
ex a, b being Element of (Omega (M -TOP_prod (M --> Sierpinski_Space))) st
( a = f . i & b = g . i & a <= b )

let i be set ; :: thesis: ( i in the carrier of X implies ex a, b being Element of (Omega (M -TOP_prod (M --> Sierpinski_Space))) st
( a = f . i & b = g . i & a <= b ) )
assume i in the carrier of X ; :: thesis: ex a, b being Element of (Omega (M -TOP_prod (M --> Sierpinski_Space))) st
( a = f . i & b = g . i & a <= b )
then reconsider x = i as Element of X ;
reconsider fx = f . x, gx = g . x as Element of (M -POS_prod (M --> (Omega Sierpinski_Space))) by A17;

now :: thesis: for j being Element of M holds fx . j <= gx . j

let j be Element of M; :: thesis: fx . j <= gx . j
A28: (M --> (oContMaps (X,Sierpinski_Space))) . j = oContMaps (X,Sierpinski_Space) by FUNCOP_1:7;
then reconsider aj = a . j, bj = b . j as continuous Function of X,(Omega Sierpinski_Space) by Th1;
a . j <= b . j by A27, WAYBEL_3:28;
then aj <= bj by A28, Th3;
then A29: ex a, b being Element of (Omega Sierpinski_Space) st
( a = aj . x & b = bj . x & a <= b ) ;
( b in the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) & G . b = commute b ) by A5;
then A30: gx . j = bj . x by A25, FUNCT_6:56;
( a in the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) & G . a = commute a ) by A5;
then fx . j = aj . x by A25, FUNCT_6:56;
hence fx . j <= gx . j by A30, A29, FUNCOP_1:7; :: thesis: verum

end;

then fx <= gx by WAYBEL_3:28;
hence ex a, b being Element of (Omega (M -TOP_prod (M --> Sierpinski_Space))) st
( a = f . i & b = g . i & a <= b ) by A17, YELLOW_0:1; :: thesis: verum

end;

then f <= g ;
hence G . a <= G . b by Th3; :: thesis: verum

end;

now :: thesis: for a being Element of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) holds (F * G) . a = (id (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))))) . a

let a be Element of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))); :: thesis: (F * G) . a = (id (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))))) . a
( a in Funcs (M, the carrier of (oContMaps (X,Sierpinski_Space))) & Funcs (M, the carrier of (oContMaps (X,Sierpinski_Space))) c= Funcs (M,(Funcs ( the carrier of X, the carrier of Sierpinski_Space))) ) by A24, Th32, FUNCT_5:56;
then A31: commute (commute a) = a by FUNCT_6:57;
thus (F * G) . a = F . (G . a) by FUNCT_2:15
.= commute (G . a) by A1
.= a by A5, A31
.= (id (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))))) . a ; :: thesis: verum

end;

then F * G = id (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) by FUNCT_2:63;
hence F is isomorphic by A18, A26, A16, YELLOW16:15; :: thesis: for f being continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)) holds F . f = commute f
let f be continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)); :: thesis: F . f = commute f
f is Element of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) by Th2;
hence F . f = commute f by A1; :: thesis: verum