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 ))
set S = Sierpinski_Space ;
set B = BoolePoset 1;
A1:
dom (Carrier (I --> (BoolePoset 1))) = I
by PARTFUN1:def 4;
A2:
dom (Carrier (I --> Sierpinski_Space )) = I
by PARTFUN1:def 4;
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 consider R being
1-sorted such that A5:
(
R = (I --> (BoolePoset 1)) . x &
(Carrier (I --> (BoolePoset 1))) . x = the
carrier of
R )
by A2, PRALG_1:def 13;
consider T being
1-sorted such that A6:
(
T = (I --> Sierpinski_Space ) . x &
(Carrier (I --> Sierpinski_Space )) . x = the
carrier of
T )
by A2, A4, PRALG_1:def 13;
thus (Carrier (I --> (BoolePoset 1))) . x =
the
carrier of
(BoolePoset 1)
by A2, A4, A5, FUNCOP_1:13
.=
bool 1
by WAYBEL_7:4
.=
the
carrier of
Sierpinski_Space
by WAYBEL18:def 9, YELLOW14:1
.=
(Carrier (I --> Sierpinski_Space )) . x
by A2, A4, A6, FUNCOP_1:13
;
:: 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:9
.=
the carrier of (product (I --> Sierpinski_Space ))
by WAYBEL18:def 3
;
:: thesis: verum