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
A1: RelStr(# the carrier of T,the InternalRel of T #) = product (I --> (BoolePoset 1)) by YELLOW_9:def 4;
A2: the topology of T = the topology of (product (I --> Sierpinski_Space )) by Th16;
set IB = I --> (BoolePoset 1);
set IS = I --> Sierpinski_Space ;
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: dom (Carrier (I --> (BoolePoset 1))) = I by PARTFUN1:def 4
.= dom (Carrier (I --> Sierpinski_Space )) by PARTFUN1:def 4 ;
A5: 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 A6: i in I by PARTFUN1:def 4;
then consider R1 being 1-sorted such that
A7: R1 = (I --> (BoolePoset 1)) . i and
A8: (Carrier (I --> (BoolePoset 1))) . i = the carrier of R1 by PRALG_1:def 13;
consider R2 being 1-sorted such that
A9: R2 = (I --> Sierpinski_Space ) . i and
A10: (Carrier (I --> Sierpinski_Space )) . i = the carrier of R2 by A6, PRALG_1:def 13;
the carrier of R1 = {0 ,1} by A3, A6, A7, FUNCOP_1:13
.= the carrier of Sierpinski_Space by Def9
.= the carrier of R2 by A6, A9, FUNCOP_1:13 ;
hence (Carrier (I --> (BoolePoset 1))) . i = (Carrier (I --> Sierpinski_Space )) . i by A8, A10; :: thesis: verum

end;

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