let X be non empty TopSpace; :: thesis:
let M be non empty set ; :: thesis:
set S = Sierpinski_Space ;
set S'M = M -TOP_prod (M --> Sierpinski_Space );
set XxxS'M = oContMaps X,(M -TOP_prod (M --> Sierpinski_Space ));
set XxS = oContMaps X,Sierpinski_Space ;
set XxS'xM = 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 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 4;
rng F c= the carrier of (M -POS_prod (M --> (oContMaps X,Sierpinski_Space )))

proof

let g be set ; :: according to TARSKI:def 3 :: thesis:
assume g in rng F ; :: thesis:
then consider f being set such that
A3: ( f in dom F & g = F . f ) by FUNCT_1:def 5;
reconsider f = f as continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space )) by A2, A3, Th2;
g = commute f by A1, A2, A3;
then reconsider g = g as Function of M,the carrier of (oContMaps X,Sierpinski_Space ) by Th32;
( 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:

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:4;
take F ; :: thesis:
deffunc H₂( Element of (M -POS_prod (M --> (oContMaps X,Sierpinski_Space )))) -> set = commute $1;
consider G being ManySortedSet of such that
A4: for f being Element of (M -POS_prod (M --> (oContMaps X,Sierpinski_Space ))) holds G . f = H₂(f) from PBOOLE:sch 5();
A5: dom G = the carrier of (M -POS_prod (M --> (oContMaps X,Sierpinski_Space ))) by PARTFUN1:def 4;
rng G c= the carrier of (oContMaps X,(M -TOP_prod (M --> Sierpinski_Space )))

proof

let g be set ; :: according to TARSKI:def 3 :: thesis:
assume g in rng G ; :: thesis:
then consider f being set such that
A6: ( f in dom G & g = G . f ) by FUNCT_1:def 5;
f in the carrier of ((oContMaps X,Sierpinski_Space ) |^ M) by A5, A6, YELLOW_1:def 5;
then f in Funcs M,the carrier of (oContMaps X,Sierpinski_Space ) by YELLOW_1:28;
then consider f' being Function such that
A7: ( f = f' & dom f' = M & rng f' c= the carrier of (oContMaps X,Sierpinski_Space ) ) by FUNCT_2:def 2;
( f' is Function of M,the carrier of (oContMaps X,Sierpinski_Space ) & g = commute f' ) by A4, A5, A6, A7, FUNCT_2:4;
then g is continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space )) by Th34;
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:

end;

then reconsider G = G as Function of (M -POS_prod (M --> (oContMaps X,Sierpinski_Space ))),(oContMaps X,(M -TOP_prod (M --> Sierpinski_Space ))) by A5, FUNCT_2:4;
A8: 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 Th33;
A9: 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 Th31
.= Funcs M,the carrier of Sierpinski_Space by CARD_3:20 ;
A10: 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 A11: 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 Th33, FUNCT_5:63;
A12: 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;
A13: 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:
assume A14: a <= b ; :: thesis:
reconsider f = a, g = b as continuous Function of X,(Omega (M -TOP_prod (M --> Sierpinski_Space ))) by Th1;
reconsider f' = a, g' = b as continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space )) by Th2;

now

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

now

let j be set ; :: thesis:
assume j in the carrier of X ; :: thesis:
then reconsider x = j as Element of X ;
reconsider fx = f . x, gx = g . x as Element of (M -POS_prod (M --> (Omega Sierpinski_Space ))) by A12;
( a in the carrier of (oContMaps X,(M -TOP_prod (M --> Sierpinski_Space ))) & b in the carrier of (oContMaps X,(M -TOP_prod (M --> Sierpinski_Space ))) ) ;
then ( F . a = commute f & F . b = commute g & a in Funcs the carrier of X,(Funcs M,the carrier of Sierpinski_Space ) & b in Funcs the carrier of X,(Funcs M,the carrier of Sierpinski_Space ) ) by A1, A8, A9;
then A16: ( Fai . x = (f' . x) . i & Fbi . x = (g' . x) . i ) by FUNCT_6:86;
f <= g by A14, Th3;
then ex a, b being Element of (Omega (M -TOP_prod (M --> Sierpinski_Space ))) st
( a = f . x & b = g . x & a <= b ) by YELLOW_2:def 1;
then fx <= gx by A12, YELLOW_0:1;
then ( fx . i <= gx . i & (M --> (Omega Sierpinski_Space )) . i = Omega Sierpinski_Space ) by FUNCOP_1:13, WAYBEL_3:28;
hence ex a, b being Element of (Omega Sierpinski_Space ) st
( a = Fai . j & b = Fbi . j & a <= b ) by A16; :: thesis:

end;

then Fai <= Fbi by YELLOW_2:def 1;
hence (F . a) . i <= (F . b) . i by A15, Th3; :: thesis:

end;

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

end;

A17: 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:
assume A18: a <= b ; :: thesis:
reconsider f = G . a, g = G . b as continuous Function of X,(Omega (M -TOP_prod (M --> Sierpinski_Space ))) by Th1;

now

let i be set ; :: thesis:
assume i in the carrier of X ; :: thesis:
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 A12;

now

let j be Element of M; :: thesis:
A19: (M --> (oContMaps X,Sierpinski_Space )) . j = oContMaps X,Sierpinski_Space by FUNCOP_1:13;
then reconsider aj = a . j, bj = b . j as continuous Function of X,(Omega Sierpinski_Space ) by Th1;
( a in the carrier of (M -POS_prod (M --> (oContMaps X,Sierpinski_Space ))) & b in the carrier of (M -POS_prod (M --> (oContMaps X,Sierpinski_Space ))) ) ;
then ( G . a = commute a & G . b = commute b & a in Funcs M,(Funcs the carrier of X,the carrier of Sierpinski_Space ) & b in Funcs M,(Funcs the carrier of X,the carrier of Sierpinski_Space ) ) by A4, A11;
then A20: ( fx . j = aj . x & gx . j = bj . x ) by FUNCT_6:86;
a . j <= b . j by A18, WAYBEL_3:28;
then aj <= bj by A19, Th3;
then ( (M --> (Omega Sierpinski_Space )) . j = Omega Sierpinski_Space & ex a, b being Element of (Omega Sierpinski_Space ) st
( a = aj . x & b = bj . x & a <= b ) ) by FUNCOP_1:13, YELLOW_2:def 1;
hence fx . j <= gx . j by A20; :: thesis:

end;

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

end;

then f <= g by YELLOW_2:def 1;
hence G . a <= G . b by Th3; :: thesis:

end;

now

let a be Element of (M -POS_prod (M --> (oContMaps X,Sierpinski_Space ))); :: thesis:
A21: a in Funcs M,the carrier of (oContMaps X,Sierpinski_Space ) by A10;
Funcs M,the carrier of (oContMaps X,Sierpinski_Space ) c= Funcs M,(Funcs the carrier of X,the carrier of Sierpinski_Space ) by Th33, FUNCT_5:63;
then A22: commute (commute a) = a by A21, FUNCT_6:87;
thus (F * G) . a = F . (G . a) by FUNCT_2:21
.= commute (G . a) by A1
.= a by A4, A22
.= (id (M -POS_prod (M --> (oContMaps X,Sierpinski_Space )))) . a by FUNCT_1:35 ; :: thesis:

end;

then A23: F * G = id (M -POS_prod (M --> (oContMaps X,Sierpinski_Space ))) by FUNCT_2:113;

now

let a be Element of (oContMaps X,(M -TOP_prod (M --> Sierpinski_Space ))); :: thesis:
a in the carrier of (oContMaps X,(M -TOP_prod (M --> Sierpinski_Space ))) ;
then A24: commute (commute a) = a by A8, A9, FUNCT_6:87;
thus (G * F) . a = G . (F . a) by FUNCT_2:21
.= commute (F . a) by A4
.= a by A1, A24
.= (id (oContMaps X,(M -TOP_prod (M --> Sierpinski_Space )))) . a by FUNCT_1:35 ; :: thesis:

end;

then G * F = id (oContMaps X,(M -TOP_prod (M --> Sierpinski_Space ))) by FUNCT_2:113;
hence F is isomorphic by A13, A17, A23, YELLOW16:17; :: thesis:
let f be continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space )); :: thesis:
f is Element of (oContMaps X,(M -TOP_prod (M --> Sierpinski_Space ))) by Th2;
hence F . f = commute f by A1; :: thesis: