set S = Sierpinski_Space ;
set B = BoolePoset 1;
let I be non empty set ; :: thesis: for T being Scott TopAugmentation of product (I --> (BoolePoset 1)) holds the carrier of T = the carrier of (product (I --> Sierpinski_Space))
let T be Scott TopAugmentation of product (I --> (BoolePoset 1)); :: thesis: the carrier of T = the carrier of (product (I --> Sierpinski_Space))
A1: dom (Carrier (I --> (BoolePoset 1))) = I by PARTFUN1:def 2;
A2: dom (Carrier (I --> Sierpinski_Space)) = I by PARTFUN1:def 2;
A3: for x being set st x in dom (Carrier (I --> Sierpinski_Space)) holds
(Carrier (I --> (BoolePoset 1))) . x = (Carrier (I --> Sierpinski_Space)) . x

proof

let x be set ; :: thesis: ( x in dom (Carrier (I --> Sierpinski_Space)) implies (Carrier (I --> (BoolePoset 1))) . x = (Carrier (I --> Sierpinski_Space)) . x )
assume A4: x in dom (Carrier (I --> Sierpinski_Space)) ; :: thesis: (Carrier (I --> (BoolePoset 1))) . 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 A2, PRALG_1:def 13;
ex R being 1-sorted st
( R = (I --> (BoolePoset 1)) . x & (Carrier (I --> (BoolePoset 1))) . x = the carrier of R ) by A2, A4, PRALG_1:def 13;
hence (Carrier (I --> (BoolePoset 1))) . x = the carrier of (BoolePoset 1) by A2, A4, FUNCOP_1:7
.= bool 1 by WAYBEL_7:2
.= the carrier of Sierpinski_Space by WAYBEL18:def 9, YELLOW14:1
.= (Carrier (I --> Sierpinski_Space)) . x by A2, A4, A5, FUNCOP_1:7 ;
:: thesis: verum

end;

RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of (product (I --> (BoolePoset 1))), the InternalRel of (product (I --> (BoolePoset 1))) #) by YELLOW_9:def 4;
hence the carrier of T = product (Carrier (I --> (BoolePoset 1))) 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