let I be non empty set ; :: thesis: for T being Scott TopAugmentation of product (I --> (BoolePoset {0})) holds T is injective
let T be Scott TopAugmentation of product (I --> (BoolePoset {0})); :: thesis: T is injective
set IB = I --> (BoolePoset {0});
set IS = I --> Sierpinski_Space;
A1: dom (Carrier (I --> (BoolePoset {0}))) = 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 Th15;
LattPOSet (BooleLatt {0}) = RelStr(# the carrier of (BooleLatt {0}),(LattRel (BooleLatt {0})) #) by LATTICE3:def 2;
then A3: the carrier of (BoolePoset {0}) = the carrier of (BooleLatt {0}) by YELLOW_1:def 2
.= bool {{}} by LATTICE3:def 1
.= {0,1} by CARD_1:49, ZFMISC_1:24 ;
A4: for i being object st i in dom (Carrier (I --> (BoolePoset {0}))) holds
(Carrier (I --> (BoolePoset {0}))) . i = (Carrier (I --> Sierpinski_Space)) . i

proof

let i be object ; :: thesis: ( i in dom (Carrier (I --> (BoolePoset {0}))) implies (Carrier (I --> (BoolePoset {0}))) . i = (Carrier (I --> Sierpinski_Space)) . i )
assume i in dom (Carrier (I --> (BoolePoset {0}))) ; :: thesis: (Carrier (I --> (BoolePoset {0}))) . i = (Carrier (I --> Sierpinski_Space)) . i
then A5: i in I ;
then consider R1 being 1-sorted such that
A6: R1 = (I --> (BoolePoset {0})) . i and
A7: (Carrier (I --> (BoolePoset {0}))) . i = the carrier of R1 by PRALG_1:def 15;
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 15;
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 {0}))) . 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 ;
then A10: product (I --> Sierpinski_Space) is injective by Th7;
RelStr(# the carrier of T, the InternalRel of T #) = product (I --> (BoolePoset {0})) by YELLOW_9:def 4;
then the carrier of T = product (Carrier (I --> (BoolePoset {0}))) 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, Th16; :: thesis: verum