set S = Sierpinski_Space ;
set B = BoolePoset {0};
let I be non empty set ; :: thesis: for T being Scott TopAugmentation of product (I --> (BoolePoset {0})) holds the carrier of T = the carrier of (product (I --> Sierpinski_Space))
let T be Scott TopAugmentation of product (I --> (BoolePoset {0})); :: thesis: the carrier of T = the carrier of (product (I --> Sierpinski_Space))
A1: dom (Carrier (I --> (BoolePoset {0}))) = I by PARTFUN1:def 2;
A2: dom (Carrier (I --> Sierpinski_Space)) = I by PARTFUN1:def 2;
A3: for x being object st x in dom (Carrier (I --> Sierpinski_Space)) holds
(Carrier (I --> (BoolePoset {0}))) . x = (Carrier (I --> Sierpinski_Space)) . x
proof
let x be object ; :: thesis: ( x in dom (Carrier (I --> Sierpinski_Space)) implies (Carrier (I --> (BoolePoset {0}))) . x = (Carrier (I --> Sierpinski_Space)) . x )
assume A4: x in dom (Carrier (I --> Sierpinski_Space)) ; :: thesis: (Carrier (I --> (BoolePoset {0}))) . x = (Carrier (I --> Sierpinski_Space)) . x
then A5: ex T being 1-sorted st
( T = (I --> Sierpinski_Space) . x & (Carrier (I --> Sierpinski_Space)) . x = the carrier of T ) by PRALG_1:def 15;
ex R being 1-sorted st
( R = (I --> (BoolePoset {0})) . x & (Carrier (I --> (BoolePoset {0}))) . x = the carrier of R ) by A4, PRALG_1:def 15;
hence (Carrier (I --> (BoolePoset {0}))) . x = the carrier of (BoolePoset {0}) by A4, FUNCOP_1:7
.= bool {0} by WAYBEL_7:2
.= the carrier of Sierpinski_Space by WAYBEL18:def 9, YELLOW14:1
.= (Carrier (I --> Sierpinski_Space)) . x by A4, A5, FUNCOP_1:7 ;
:: thesis: verum
end;
RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of (product (I --> (BoolePoset {0}))), the InternalRel of (product (I --> (BoolePoset {0}))) #) by YELLOW_9:def 4;
hence the carrier of T = product (Carrier (I --> (BoolePoset {0}))) by YELLOW_1:def 4
.= product (Carrier (I --> Sierpinski_Space)) by A1, A2, A3, FUNCT_1:2
.= the carrier of (product (I --> Sierpinski_Space)) by WAYBEL18:def 3 ;
:: thesis: verum