let I be non empty set ; :: thesis:
set IS = I --> Sierpinski_Space ;
set pB = { (product ((Carrier (I --> Sierpinski_Space )) +* i,{1})) where i is Element of I : verum } ;
set P = product_prebasis (I --> Sierpinski_Space );
A1: product_prebasis (I --> Sierpinski_Space ) is prebasis of (product (I --> Sierpinski_Space )) by Def3;
then A2: product_prebasis (I --> Sierpinski_Space ) c= the topology of (product (I --> Sierpinski_Space )) by TOPS_2:78;
{ (product ((Carrier (I --> Sierpinski_Space )) +* i,{1})) where i is Element of I : verum } c= bool the carrier of (product (I --> Sierpinski_Space ))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { (product ((Carrier (I --> Sierpinski_Space )) +* i,{1})) where i is Element of I : verum } ; :: thesis:
then consider i being Element of I such that
A3: x = product ((Carrier (I --> Sierpinski_Space )) +* i,{1}) ;
product ((Carrier (I --> Sierpinski_Space )) +* i,{1}) c= product (Carrier (I --> Sierpinski_Space ))

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in product ((Carrier (I --> Sierpinski_Space )) +* i,{1}) ; :: thesis:
then consider g being Function such that
A4: y = g and
A5: dom g = dom ((Carrier (I --> Sierpinski_Space )) +* i,{1}) and
A6: for z being set st z in dom ((Carrier (I --> Sierpinski_Space )) +* i,{1}) holds
g . z in ((Carrier (I --> Sierpinski_Space )) +* i,{1}) . z by CARD_3:def 5;
A7: for z being set st z in dom (Carrier (I --> Sierpinski_Space )) holds
g . z in (Carrier (I --> Sierpinski_Space )) . z

proof

let z be set ; :: thesis:
assume A8: z in dom (Carrier (I --> Sierpinski_Space )) ; :: thesis:
then A9: z in I by PARTFUN1:def 4;
then consider R being 1-sorted such that
A10: R = (I --> Sierpinski_Space ) . z and
A11: (Carrier (I --> Sierpinski_Space )) . z = the carrier of R by PRALG_1:def 13;
A12: the carrier of R = the carrier of Sierpinski_Space by A9, A10, FUNCOP_1:13
.= {0 ,1} by Def9 ;
z in dom ((Carrier (I --> Sierpinski_Space )) +* i,{1}) by A8, FUNCT_7:32;
then A13: g . z in ((Carrier (I --> Sierpinski_Space )) +* i,{1}) . z by A6;

per cases ;

suppose z = i ; :: thesis:

then ((Carrier (I --> Sierpinski_Space )) +* i,{1}) . z = {1} by A8, FUNCT_7:33;
then g . z = 1 by A13, TARSKI:def 1;
hence g . z in (Carrier (I --> Sierpinski_Space )) . z by A11, A12, TARSKI:def 2; :: thesis:

end;

suppose z <> i ; :: thesis:

hence g . z in (Carrier (I --> Sierpinski_Space )) . z by A13, FUNCT_7:34; :: thesis:

end;

end;

end;

dom g = dom (Carrier (I --> Sierpinski_Space )) by A5, FUNCT_7:32;
hence y in product (Carrier (I --> Sierpinski_Space )) by A4, A7, CARD_3:def 5; :: thesis:

end;

then x c= the carrier of (product (I --> Sierpinski_Space )) by A3, Def3;
hence x in bool the carrier of (product (I --> Sierpinski_Space )) ; :: thesis:

end;

then reconsider B = { (product ((Carrier (I --> Sierpinski_Space )) +* i,{1})) where i is Element of I : verum } as Subset-Family of (product (I --> Sierpinski_Space )) ;
reconsider B = B as Subset-Family of (product (I --> Sierpinski_Space )) ;
A14: B c= product_prebasis (I --> Sierpinski_Space )

proof

{1} c= {0 ,1} by ZFMISC_1:12;
then reconsider V = {1} as Subset of Sierpinski_Space by Def9;
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A15: x in B ; :: thesis:
then consider i being Element of I such that
A16: x = product ((Carrier (I --> Sierpinski_Space )) +* i,{1}) ;
reconsider y = x as Subset of (product (Carrier (I --> Sierpinski_Space ))) by A15, Def3;
{1} in {{} ,{1},{0 ,1}} by ENUMSET1:def 1;
then {1} in the topology of Sierpinski_Space by Def9;
then A17: V is open by PRE_TOPC:def 5;
( Sierpinski_Space = (I --> Sierpinski_Space ) . i & y = product ((Carrier (I --> Sierpinski_Space )) +* i,V) ) by A16, FUNCOP_1:13;
hence x in product_prebasis (I --> Sierpinski_Space ) by A17, Def2; :: thesis:

end;

reconsider P = product_prebasis (I --> Sierpinski_Space ) as Subset-Family of (product (I --> Sierpinski_Space )) by Def3;
reconsider P = P as Subset-Family of (product (I --> Sierpinski_Space )) ;
FinMeetCl P is Basis of (product (I --> Sierpinski_Space )) by A1, YELLOW_9:23;
then reconsider F = (FinMeetCl P) \ {{} } as Basis of (product (I --> Sierpinski_Space )) by Th3;
A18: F c= FinMeetCl B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A19: x in F ; :: thesis:
then reconsider y = x as Subset of (product (I --> Sierpinski_Space )) ;
x in FinMeetCl P by A19, XBOOLE_0:def 5;
then consider Y1 being Subset-Family of (product (I --> Sierpinski_Space )) such that
A20: Y1 c= P and
A21: Y1 is finite and
A22: y = Intersect Y1 by CANTOR_1:def 4;
reconsider Y2 = Y1 /\ B as Subset-Family of (product (I --> Sierpinski_Space )) ;
A23: ( Y2 c= B & Y2 is finite ) by A21, FINSET_1:13, XBOOLE_1:17;
A24: the carrier of (product (I --> Sierpinski_Space )) = product (Carrier (I --> Sierpinski_Space )) by Def3;
A25: not x in {{} } by A19, XBOOLE_0:def 5;
A26: Intersect Y2 c= Intersect Y1

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A27: z in Intersect Y2 ; :: thesis:
then A28: z in product (Carrier (I --> Sierpinski_Space )) by A24;
for Y being set st Y in Y1 holds
z in Y

proof

let Y be set ; :: thesis:
assume A29: Y in Y1 ; :: thesis:
then reconsider Y9 = Y as Subset of (product (Carrier (I --> Sierpinski_Space ))) by Def3;
consider i being set , S being TopStruct , V being Subset of S such that
A30: i in I and
A31: V is open and
A32: S = (I --> Sierpinski_Space ) . i and
A33: Y9 = product ((Carrier (I --> Sierpinski_Space )) +* i,V) by A20, A29, Def2;
reconsider V9 = V as Subset of Sierpinski_Space by A30, A32, FUNCOP_1:13;
V in the topology of S by A31, PRE_TOPC:def 5;
then V9 in the topology of Sierpinski_Space by A30, A32, FUNCOP_1:13;
then A34: V9 in {{} ,{1},{0 ,1}} by Def9;
A35: i in dom (Carrier (I --> Sierpinski_Space )) by A30, PARTFUN1:def 4;
A36: V9 <> {}

proof

( ((Carrier (I --> Sierpinski_Space )) +* i,{} ) . i = {} & i in dom ((Carrier (I --> Sierpinski_Space )) +* i,{} ) ) by A35, FUNCT_7:32, FUNCT_7:33;
then A37: {} in rng ((Carrier (I --> Sierpinski_Space )) +* i,{} ) by FUNCT_1:def 5;
assume V9 = {} ; :: thesis:
then Y9 = {} by A33, A37, CARD_3:37;
then y = {} by A22, A29, MSSUBFAM:3;
hence contradiction by A25, TARSKI:def 1; :: thesis:

end;

reconsider i9 = i as Element of I by A30;
A38: ex RR being 1-sorted st
( RR = (I --> Sierpinski_Space ) . i & (Carrier (I --> Sierpinski_Space )) . i = the carrier of RR ) by A30, PRALG_1:def 13;

per cases by A34, A36, ENUMSET1:def 1;

suppose V9 = {1} ; :: thesis:

then Y9 = product ((Carrier (I --> Sierpinski_Space )) +* i9,{1}) by A33;
then Y in B ;
then Y in Y2 by A29, XBOOLE_0:def 4;
hence z in Y by A27, SETFAM_1:58; :: thesis:

end;

suppose V9 = {0 ,1} ; :: thesis:

then V9 = the carrier of Sierpinski_Space by Def9
.= (Carrier (I --> Sierpinski_Space )) . i by A30, A38, FUNCOP_1:13 ;
hence z in Y by A28, A33, FUNCT_7:37; :: thesis:

end;

end;

end;

hence z in Intersect Y1 by A27, SETFAM_1:58; :: thesis:

end;

Intersect Y1 c= Intersect Y2 by SETFAM_1:59, XBOOLE_1:17;
then y = Intersect Y2 by A22, A26, XBOOLE_0:def 10;
hence x in FinMeetCl B by A23, CANTOR_1:def 4; :: thesis:

end;

{ (product ((Carrier (I --> Sierpinski_Space )) +* i,{1})) where i is Element of I : verum } c= the topology of (product (I --> Sierpinski_Space )) by A14, A2, XBOOLE_1:1;
hence { (product ((Carrier (I --> Sierpinski_Space )) +* i,{1})) where i is Element of I : verum } is prebasis of (product (I --> Sierpinski_Space )) by A18, CANTOR_1:def 5, TOPS_2:78; :: thesis: