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:64;
{ (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 object ; :: according to TARSKI:def 3 :: thesis:
reconsider xx = x as set by TARSKI:1;
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 object ; :: 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 object 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 object st z in dom (Carrier (I --> Sierpinski_Space)) holds
g . z in (Carrier (I --> Sierpinski_Space)) . z

proof

let z be object ; :: thesis:
assume A8: z in dom (Carrier (I --> Sierpinski_Space)) ; :: thesis:
then A9: z in I ;
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 15;
A12: the carrier of R = the carrier of Sierpinski_Space by A9, A10, FUNCOP_1:7
.= {0,1} by Def9 ;
z in dom ((Carrier (I --> Sierpinski_Space)) +* (i,{1})) by A8, FUNCT_7:30;
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:31;
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:32; :: thesis:

end;

end;

end;

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

end;

then xx 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:7;
then reconsider V = {1} as Subset of Sierpinski_Space by Def9;
let x be object ; :: 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 ;
( Sierpinski_Space = (I --> Sierpinski_Space) . i & y = product ((Carrier (I --> Sierpinski_Space)) +* (i,V)) ) by A16;
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 Th2;
A18: F c= FinMeetCl B

proof

let x be object ; :: 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 3;
reconsider Y2 = Y1 /\ B as Subset-Family of (product (I --> Sierpinski_Space)) ;
A23: ( Y2 c= B & Y2 is finite ) by A21, FINSET_1:1, 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 object ; :: 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:7;
V in the topology of S by A31;
then V9 in the topology of Sierpinski_Space by A30, A32, FUNCOP_1:7;
then A34: V9 in {{},{1},{0,1}} by Def9;
A35: i in dom (Carrier (I --> Sierpinski_Space)) by A30, PARTFUN1:def 2;
A36: V9 <> {}

proof

( ((Carrier (I --> Sierpinski_Space)) +* (i,{})) . i = {} & i in dom ((Carrier (I --> Sierpinski_Space)) +* (i,{})) ) by A35, FUNCT_7:30, FUNCT_7:31;
then A37: {} in rng ((Carrier (I --> Sierpinski_Space)) +* (i,{})) by FUNCT_1:def 3;
assume V9 = {} ; :: thesis:
then Y9 = {} by A33, A37, CARD_3:26;
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 15;

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:43; :: 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:7 ;
hence z in Y by A28, A33, FUNCT_7:35; :: thesis:

end;

end;

end;

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

end;

Intersect Y1 c= Intersect Y2 by SETFAM_1:44, XBOOLE_1:17;
then y = Intersect Y2 by A22, A26;
hence x in FinMeetCl B by A23, CANTOR_1:def 3; :: 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;
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 4, TOPS_2:64; :: thesis: