set SS = Sierpinski_Space ;
set B = BoolePoset {0};
let T be injective T_0-TopSpace; :: thesis: for S being Scott TopAugmentation of Omega T holds TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #)
let S be Scott TopAugmentation of Omega T; :: thesis: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #)
consider M being non empty set such that
A1: T is_Retract_of product (M --> Sierpinski_Space) by WAYBEL18:19;
consider c being continuous Function of T,(product (M --> Sierpinski_Space)), r being continuous Function of (product (M --> Sierpinski_Space)),T such that
A2: r * c = id T by A1;
A3: TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) by Def2;
A4: TopStruct(# the carrier of (product (M --> Sierpinski_Space)), the topology of (product (M --> Sierpinski_Space)) #) = TopStruct(# the carrier of (Omega (product (M --> Sierpinski_Space))), the topology of (Omega (product (M --> Sierpinski_Space))) #) by Def2;
then reconsider c1a = c as Function of (Omega T),(Omega (product (M --> Sierpinski_Space))) by A3;
set S2M = the Scott TopAugmentation of product (M --> (BoolePoset {0}));
A5: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of S, the topology of S #) ;
A6: RelStr(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset {0})), the InternalRel of the Scott TopAugmentation of product (M --> (BoolePoset {0})) #) = RelStr(# the carrier of (product (M --> (BoolePoset {0}))), the InternalRel of (product (M --> (BoolePoset {0}))) #) by YELLOW_9:def 4;
then reconsider c1 = c as Function of (Omega T),(product (M --> (BoolePoset {0}))) by A3, Th3;
A7: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (Omega T), the InternalRel of (Omega T) #) by YELLOW_9:def 4;
then reconsider c2 = c1 as Function of S, the Scott TopAugmentation of product (M --> (BoolePoset {0})) by A6;
A8: the carrier of the Scott TopAugmentation of product (M --> (BoolePoset {0})) = the carrier of (product (M --> Sierpinski_Space)) by Th3;
then reconsider rr = r as Function of the Scott TopAugmentation of product (M --> (BoolePoset {0})),T ;
A9: the topology of the Scott TopAugmentation of product (M --> (BoolePoset {0})) = the topology of (product (M --> Sierpinski_Space)) by WAYBEL18:15;
then reconsider W = T as non empty monotone-convergence TopSpace by A1, A8, Th36;
Omega (product (M --> Sierpinski_Space)) = Omega the Scott TopAugmentation of product (M --> (BoolePoset {0})) by A9, A8, Th13;
then A10: RelStr(# the carrier of (Omega (product (M --> Sierpinski_Space))), the InternalRel of (Omega (product (M --> Sierpinski_Space))) #) = RelStr(# the carrier of (product (M --> (BoolePoset {0}))), the InternalRel of (product (M --> (BoolePoset {0}))) #) by Th16
.= RelStr(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset {0})), the InternalRel of the Scott TopAugmentation of product (M --> (BoolePoset {0})) #) by YELLOW_9:def 4 ;
reconsider r1 = r as Function of (product (M --> (BoolePoset {0}))),(Omega T) by A8, A6, A3;
A11: RelStr(# the carrier of (Omega the Scott TopAugmentation of product (M --> (BoolePoset {0}))), the InternalRel of (Omega the Scott TopAugmentation of product (M --> (BoolePoset {0}))) #) = RelStr(# the carrier of (product (M --> (BoolePoset {0}))), the InternalRel of (product (M --> (BoolePoset {0}))) #) by Th16;
then reconsider rr1 = r1 as Function of (Omega the Scott TopAugmentation of product (M --> (BoolePoset {0}))),(Omega T) ;
reconsider r2 = r1 as Function of the Scott TopAugmentation of product (M --> (BoolePoset {0})),S by A6, A7;
reconsider r3 = r2 as Function of (product (M --> Sierpinski_Space)),S by Th3;
TopStruct(# the carrier of (Omega the Scott TopAugmentation of product (M --> (BoolePoset {0}))), the topology of (Omega the Scott TopAugmentation of product (M --> (BoolePoset {0}))) #) = TopStruct(# the carrier of the Scott TopAugmentation of product (M --> (BoolePoset {0})), the topology of the Scott TopAugmentation of product (M --> (BoolePoset {0})) #) by Def2;
then rr1 is continuous by A9, A8, A3, YELLOW12:36;
then r2 is directed-sups-preserving by A6, A7, A11, WAYBEL21:6;
then r3 is continuous by A9, A8, A5, YELLOW12:36;
then A12: r3 * c is continuous ;
reconsider c1a = c1a as continuous Function of (Omega W),(Omega (product (M --> Sierpinski_Space))) by A3, A4, YELLOW12:36;
c2 = c1a ;
then A13: c2 is directed-sups-preserving by A7, A10, WAYBEL21:6;
TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of T, the topology of T #) ;
then rr is continuous by A9, A8, YELLOW12:36;
then rr * c2 is continuous by A13;
hence TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) by A2, A12, YELLOW14:33; :: thesis: verum