let I be non empty set ; :: thesis: for T being Scott TopAugmentation of product (I --> (BoolePoset 1)) holds T is injective
let T be Scott TopAugmentation of product (I --> (BoolePoset 1)); :: thesis: T is injective
set IB = I --> (BoolePoset 1);
set IS = I --> Sierpinski_Space ;
A1: dom (Carrier (I --> (BoolePoset 1))) = I by PARTFUN1:def 4
.= dom (Carrier (I --> Sierpinski_Space )) by PARTFUN1:def 4 ;
A2: the topology of T = the topology of (product (I --> Sierpinski_Space )) by Th16;
LattPOSet (BooleLatt 1) = RelStr(# the carrier of (BooleLatt 1),(LattRel (BooleLatt 1)) #) by LATTICE3:def 2;
then A3: the carrier of (BoolePoset 1) = the carrier of (BooleLatt 1) by YELLOW_1:def 2
.= bool {{} } by CARD_1:87, LATTICE3:def 1
.= {0 ,1} by CARD_1:87, ZFMISC_1:30 ;
A4: for i being set st i in dom (Carrier (I --> (BoolePoset 1))) holds
(Carrier (I --> (BoolePoset 1))) . i = (Carrier (I --> Sierpinski_Space )) . i

proof

let i be set ; :: thesis: ( i in dom (Carrier (I --> (BoolePoset 1))) implies (Carrier (I --> (BoolePoset 1))) . i = (Carrier (I --> Sierpinski_Space )) . i )
assume i in dom (Carrier (I --> (BoolePoset 1))) ; :: thesis: (Carrier (I --> (BoolePoset 1))) . i = (Carrier (I --> Sierpinski_Space )) . i
then A5: i in I by PARTFUN1:def 4;
then consider R1 being 1-sorted such that
A6: R1 = (I --> (BoolePoset 1)) . i and
A7: (Carrier (I --> (BoolePoset 1))) . i = the carrier of R1 by PRALG_1:def 13;
consider R2 being 1-sorted such that
A8: R2 = (I --> Sierpinski_Space ) . i and
A9: (Carrier (I --> Sierpinski_Space )) . i = the carrier of R2 by A5, PRALG_1:def 13;
the carrier of R1 = {0 ,1} by A3, A5, A6, FUNCOP_1:13
.= the carrier of Sierpinski_Space by Def9
.= the carrier of R2 by A5, A8, FUNCOP_1:13 ;
hence (Carrier (I --> (BoolePoset 1))) . i = (Carrier (I --> Sierpinski_Space )) . i by A7, A9; :: thesis: verum

end;

for i being Element of I holds (I --> Sierpinski_Space ) . i is injective by FUNCOP_1:13;
then A10: product (I --> Sierpinski_Space ) is injective by Th8;
RelStr(# the carrier of T,the InternalRel of T #) = product (I --> (BoolePoset 1)) by YELLOW_9:def 4;
then the carrier of T = product (Carrier (I --> (BoolePoset 1))) by YELLOW_1:def 4
.= product (Carrier (I --> Sierpinski_Space )) by A1, A4, FUNCT_1:9
.= the carrier of (product (I --> Sierpinski_Space )) by Def3 ;
hence T is injective by A2, A10, Th17; :: thesis: verum