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 2
.= dom (Carrier (I --> Sierpinski_Space)) by PARTFUN1:def 2 ;
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:49, LATTICE3:def 1
.= {0,1} by CARD_1:49, ZFMISC_1:24 ;
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 2;
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:7
.= the carrier of Sierpinski_Space by Def9
.= the carrier of R2 by A5, A8, FUNCOP_1:7 ;
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:7;
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:2
.= the carrier of (product (I --> Sierpinski_Space)) by Def3 ;
hence T is injective by A2, A10, Th17; :: thesis: verum