let I be non empty set ; :: thesis:
let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis:
let P be Subset of (product (Carrier J)); :: thesis:
assume A1: P in FinMeetCl (product_prebasis J) ; :: thesis:
consider Y being Subset-Family of (product (Carrier J)) such that
A2: ( Y c= product_prebasis J & Y is finite & P = Intersect Y ) by A1, CANTOR_1:def 3;

suppose A3: ( not Y is empty & meet Y <> {} ) ; :: thesis:

then A4: P = meet Y by A2, SETFAM_1:def 9;
defpred S₁[ object , object ] means ex i being Element of I ex B being Subset of (J . i) st
( $2 = i & B is open & $1 = product ((Carrier J) +* (i,B)) );
A5: for x being object st x in Y holds
ex i being object st
( i in I & S₁[x,i] )

proof

let x be object ; :: thesis:
assume x in Y ; :: thesis:
then consider i being set , T being TopStruct , V being Subset of T such that
A6: ( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) by A2, WAYBEL18:def 2;
take i ; :: thesis:
thus i in I by A6; :: thesis:
reconsider j = i as Element of I by A6;
reconsider V = V as Subset of (J . j) by A6;
take j ; :: thesis:
take V ; :: thesis:
thus ( i = j & V is open & x = product ((Carrier J) +* (j,V)) ) by A6; :: thesis:

end;

consider g being Function of Y,I such that
A7: for x being object st x in Y holds
S₁[x,g . x] from FUNCT_2:sch 1(A5);
set X = { (meet (g " {i})) where i is Element of I : g " {i} <> {} } ;
{ (meet (g " {i})) where i is Element of I : g " {i} <> {} } c= bool (product (Carrier J))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { (meet (g " {i})) where i is Element of I : g " {i} <> {} } ; :: thesis:
then consider i being Element of I such that
A8: ( x = meet (g " {i}) & g " {i} <> {} ) ;
reconsider Z = g " {i} as Subset-Family of (product (Carrier J)) by XBOOLE_1:1;
meet Z is Subset of (product (Carrier J)) ;
hence x in bool (product (Carrier J)) by A8; :: thesis:

end;

then reconsider X = { (meet (g " {i})) where i is Element of I : g " {i} <> {} } as Subset-Family of (product (Carrier J)) ;
take X ; :: thesis:
defpred S₂[ object , object ] means ex i being Element of I st
( $2 = i & $1 = meet (g " {i}) & g " {i} <> {} );
A9: for x being object st x in X holds
ex i being object st
( i in I & S₂[x,i] )

proof

let x be object ; :: thesis:
assume x in X ; :: thesis:
then consider i being Element of I such that
A10: ( x = meet (g " {i}) & g " {i} <> {} ) ;
take i ; :: thesis:
thus i in I ; :: thesis:
take i ; :: thesis:
thus ( i = i & x = meet (g " {i}) & g " {i} <> {} ) by A10; :: thesis:

end;

consider f being Function of X,I such that
A11: for x being object st x in X holds
S₂[x,f . x] from FUNCT_2:sch 1(A9);
A12: ( dom f = X & rng f c= I ) by FUNCT_2:def 1;
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis:
assume A13: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis:
then consider i1 being Element of I such that
A14: ( f . x1 = i1 & x1 = meet (g " {i1}) & g " {i1} <> {} ) by A11;
ex i2 being Element of I st
( f . x2 = i2 & x2 = meet (g " {i2}) & g " {i2} <> {} ) by A11, A13;
hence x1 = x2 by A13, A14; :: thesis:

end;

then reconsider f = f as I -valued one-to-one Function by FUNCT_1:def 4;
take f ; :: thesis:
A16: for i being Element of I
for S being non empty set st g " {i} <> {} & S in g " {i} holds
ex V being non empty open Subset of (J . i) st S = product ((Carrier J) +* (i,V))

proof

let i be Element of I; :: thesis:
let S be non empty set ; :: thesis:
assume a17: ( g " {i} <> {} & S in g " {i} ) ; :: thesis:
then A17: ( S in Y & g . S in {i} ) by FUNCT_2:38;
then consider j being set , T being TopStruct , V being Subset of T such that
A18: ( j in I & V is open & T = J . j ) and
A19: S = product ((Carrier J) +* (j,V)) by A2, WAYBEL18:def 2;
a20: dom (Carrier J) = I by PARTFUN1:def 2;

per cases ;

suppose A21: V <> (Carrier J) . j ; :: thesis:

A22: not V is empty by A19, a20, Th36, A18;
A23: i = j

proof

g . S = i by A17, TARSKI:def 1;
then consider k being Element of I, B being Subset of (J . k) such that
A24: ( i = k & B is open ) and
A25: S = product ((Carrier J) +* (k,B)) by A7, a17;
not B is empty by a20, A25, Th36;
hence i = j by A19, A18, a20, A21, A22, A24, A25, Th42; :: thesis:

end;

then reconsider V = V as non empty open Subset of (J . i) by A19, a20, Th36, A18;
take V ; :: thesis:
thus S = product ((Carrier J) +* (i,V)) by A19, A23; :: thesis:

end;

suppose V = (Carrier J) . j ; :: thesis:

then A26: S = product (Carrier J) by A19, FUNCT_7:35
.= product ((Carrier J) +* (i,((Carrier J) . i))) by FUNCT_7:35 ;
take [#] (J . i) ; :: thesis:
thus S = product ((Carrier J) +* (i,([#] (J . i)))) by A26, PENCIL_3:7; :: thesis:

end;

A27: not X is empty

proof

A28: ex i being Element of I st g " {i} <> {}

proof

set A = the Element of Y;
consider i being Element of I, B being Subset of (J . i) such that
A29: ( g . the Element of Y = i & B is open & the Element of Y = product ((Carrier J) +* (i,B)) ) by A3, A7;
take i ; :: thesis:
g . the Element of Y in {i} by A29, TARSKI:def 1;
hence g " {i} <> {} by A3, FUNCT_2:38; :: thesis:

end;

ex x being object st x in X

proof

consider i being Element of I such that
A30: g " {i} <> {} by A28;
meet (g " {i}) in X by A30;
hence ex x being object st x in X ; :: thesis:

end;

hence not X is empty ; :: thesis:

end;

A31: for x being Element of X st x = meet (g " {(f . x)}) & g " {(f . x)} <> {} & x <> {} holds
ex Z being Subset-Family of (J . (In ((f . x),I))) st
( Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } & Z is open & Z is finite & not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) )

proof

let x be Element of X; :: thesis:
set i = In ((f . x),I);
a32: f . x in rng f by A12, A27, FUNCT_1:3;
then A32: In ((f . x),I) = f . x by SUBSET_1:def 8;
assume A33: ( x = meet (g " {(f . x)}) & g " {(f . x)} <> {} & x <> {} ) ; :: thesis:
set Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } ;
{ ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } c= bool the carrier of (J . (In ((f . x),I)))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } ; :: thesis:
then ex V being Subset of (product (Carrier J)) st
( y = (proj (J,(In ((f . x),I)))) .: V & V in g " {(f . x)} ) ;
hence y in bool the carrier of (J . (In ((f . x),I))) ; :: thesis:

end;

then reconsider Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } as Subset-Family of (J . (In ((f . x),I))) ;
take Z ; :: thesis:
thus Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } ; :: thesis:
for A being Subset of (J . (In ((f . x),I))) st A in Z holds
A is open

proof

let A be Subset of (J . (In ((f . x),I))); :: thesis:
assume A in Z ; :: thesis:
then consider V being Subset of (product (Carrier J)) such that
A35: ( A = (proj (J,(In ((f . x),I)))) .: V & V in g " {(f . x)} ) ;
( V in Y & ( V is empty or not V is empty ) ) by A35;
hence A is open by A2, A35, Th58; :: thesis:

end;

hence Z is open by TOPS_2:def 1; :: thesis:
defpred S₃[ object , object ] means ex V being Subset of (product (Carrier J)) st
( $1 = V & $2 = (proj (J,(In ((f . x),I)))) .: V );
A37: for y, z1, z2 being object st y in g " {(In ((f . x),I))} & S₃[y,z1] & S₃[y,z2] holds
z1 = z2 ;
A38: for y being object st y in g " {(In ((f . x),I))} holds
ex z being object st S₃[y,z]

proof

let y be object ; :: thesis:
assume y in g " {(In ((f . x),I))} ; :: thesis:
then y in Y ;
then reconsider V = y as Subset of (product (Carrier J)) ;
take (proj (J,(In ((f . x),I)))) .: V ; :: thesis:
take V ; :: thesis:
thus ( y = V & (proj (J,(In ((f . x),I)))) .: V = (proj (J,(In ((f . x),I)))) .: V ) ; :: thesis:

end;

consider h being Function such that
A39: ( dom h = g " {(In ((f . x),I))} & ( for y being object st y in g " {(In ((f . x),I))} holds
S₃[y,h . y] ) ) from FUNCT_1:sch 2(A37, A38);
a45: for y being object holds
( y in rng h iff y in Z )

proof

let y be object ; :: thesis:

hereby :: thesis:

assume y in rng h ; :: thesis:
then consider z being object such that
A40: ( z in dom h & y = h . z ) by FUNCT_1:def 3;
ex V being Subset of (product (Carrier J)) st
( z = V & h . z = (proj (J,(In ((f . x),I)))) .: V ) by A39, A40;
hence y in Z by A32, A39, A40; :: thesis:

end;

assume y in Z ; :: thesis:
then consider V being Subset of (product (Carrier J)) such that
A42: ( y = (proj (J,(In ((f . x),I)))) .: V & V in g " {(f . x)} ) ;
A43: V in dom h by a32, SUBSET_1:def 8, A39, A42;
ex V0 being Subset of (product (Carrier J)) st
( V = V0 & h . V = (proj (J,(In ((f . x),I)))) .: V0 ) by A32, A39, A42;
hence y in rng h by A42, A43, FUNCT_1:def 3; :: thesis:

end;

then rng h = Z by TARSKI:2;
hence Z is finite by A2, A39, FINSET_1:8; :: thesis:
h . the Element of g " {(f . x)} in rng h by A32, A33, A39, FUNCT_1:3;
hence A46: not Z is empty by a45; :: thesis:
a47: dom (Carrier J) = I by PARTFUN1:def 2;
then A47: In ((f . x),I) in dom (Carrier J) ;
for y being object holds
( y in meet (g " {(In ((f . x),I))}) iff y in product ((Carrier J) +* ((In ((f . x),I)),(meet Z))) )

proof

let y be object ; :: thesis:

hereby :: thesis:

assume A49: y in meet (g " {(In ((f . x),I))}) ; :: thesis:
set S0 = the Element of g " {(In ((f . x),I))};
not the Element of g " {(In ((f . x),I))} is empty by A32, A33, A49, SETFAM_1:def 1;
then consider V0 being non empty open Subset of (J . (In ((f . x),I))) such that
A50: the Element of g " {(In ((f . x),I))} = product ((Carrier J) +* ((In ((f . x),I)),V0)) by A16, A32, A33;
y in product ((Carrier J) +* ((In ((f . x),I)),V0)) by A32, A33, A49, A50, SETFAM_1:def 1;
then consider f0 being Function such that
A51: ( y = f0 & dom f0 = dom ((Carrier J) +* ((In ((f . x),I)),V0)) ) and
A52: for z being object st z in dom ((Carrier J) +* ((In ((f . x),I)),V0)) holds
f0 . z in ((Carrier J) +* ((In ((f . x),I)),V0)) . z by CARD_3:def 5;

now :: thesis:

take f0 = f0; :: thesis:
thus y = f0 by A51; :: thesis:
thus dom f0 = dom (Carrier J) by A51, FUNCT_7:30
.= dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) by FUNCT_7:30 ; :: thesis:
let z be object ; :: thesis:
assume z in dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) ; :: thesis:
then A53: z in dom (Carrier J) by FUNCT_7:30;

per cases ;

suppose A54: z <> In ((f . x),I) ; :: thesis:

then A55: ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . z = (Carrier J) . z by FUNCT_7:32
.= ((Carrier J) +* ((In ((f . x),I)),V0)) . z by A54, FUNCT_7:32 ;
z in dom ((Carrier J) +* ((In ((f . x),I)),V0)) by A53, FUNCT_7:30;
hence f0 . z in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . z by A52, A55; :: thesis:

end;

suppose A56: z = In ((f . x),I) ; :: thesis:

then A57: ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . z = meet Z by A53, FUNCT_7:31;
for S being set st S in Z holds
f0 . z in S

proof

let S be set ; :: thesis:
assume S in Z ; :: thesis:
then consider S1 being Subset of (product (Carrier J)) such that
A58: ( S = (proj (J,(In ((f . x),I)))) .: S1 & S1 in g " {(f . x)} ) ;
not S1 is empty by A32, A49, A58, SETFAM_1:def 1;
then consider V1 being non empty open Subset of (J . (In ((f . x),I))) such that
A59: S1 = product ((Carrier J) +* ((In ((f . x),I)),V1)) by A16, A32, A58;
V1 c= the carrier of (J . (In ((f . x),I))) ;
then V1 c= [#] (J . (In ((f . x),I))) by STRUCT_0:def 3;
then A60: V1 c= (Carrier J) . (In ((f . x),I)) by PENCIL_3:7;
proj (J,(In ((f . x),I))) = proj ((Carrier J),(In ((f . x),I))) by WAYBEL18:def 4;
then A61: S = V1 by A58, A59, A60, a47, Th43;
y in S1 by A32, A49, A58, SETFAM_1:def 1;
then consider f1 being Function such that
A62: ( y = f1 & dom f1 = dom ((Carrier J) +* ((In ((f . x),I)),V1)) ) and
A63: for a being object st a in dom ((Carrier J) +* ((In ((f . x),I)),V1)) holds
f1 . a in ((Carrier J) +* ((In ((f . x),I)),V1)) . a by A59, CARD_3:def 5;
In ((f . x),I) in dom ((Carrier J) +* ((In ((f . x),I)),V1)) by A47, FUNCT_7:30;
then f1 . (In ((f . x),I)) in ((Carrier J) +* ((In ((f . x),I)),V1)) . (In ((f . x),I)) by A63;
hence f0 . z in S by A51, A56, A61, A62, a47, FUNCT_7:31; :: thesis:

end;

hence f0 . z in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . z by A57, A46, SETFAM_1:def 1; :: thesis:

end;

hence y in product ((Carrier J) +* ((In ((f . x),I)),(meet Z))) by CARD_3:def 5; :: thesis:

end;

assume A64: y in product ((Carrier J) +* ((In ((f . x),I)),(meet Z))) ; :: thesis:
for S being set st S in g " {(In ((f . x),I))} holds
y in S

proof

let S be set ; :: thesis:
assume A65: S in g " {(In ((f . x),I))} ; :: thesis:
not S is empty by A32, A33, A65, SETFAM_1:4;
then consider V being non empty open Subset of (J . (In ((f . x),I))) such that
A66: S = product ((Carrier J) +* ((In ((f . x),I)),V)) by A16, A65;
V c= the carrier of (J . (In ((f . x),I))) ;
then V c= [#] (J . (In ((f . x),I))) by STRUCT_0:def 3;
then A67: V c= (Carrier J) . (In ((f . x),I)) by PENCIL_3:7;
proj (J,(In ((f . x),I))) = proj ((Carrier J),(In ((f . x),I))) by WAYBEL18:def 4;
then A68: (proj (J,(In ((f . x),I)))) .: S = V by a47, A66, A67, Th43;
S in Y by A65;
then V in Z by A32, A65, A68;
then product ((Carrier J) +* ((In ((f . x),I)),(meet Z))) c= product ((Carrier J) +* ((In ((f . x),I)),V)) by a47, Th38, SETFAM_1:3;
hence y in S by A64, A66; :: thesis:

end;

hence y in meet (g " {(In ((f . x),I))}) by A32, A33, SETFAM_1:def 1; :: thesis:

end;

hence x = product ((Carrier J) +* ((f . x),(meet Z))) by A32, A33, TARSKI:2; :: thesis:

end;

for x being object st x in X holds
x in product_prebasis J

proof

let x be object ; :: thesis:
assume A69: x in X ; :: thesis:

per cases ;

suppose A70: x <> {} ; :: thesis:

ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) )

proof

consider i being Element of I such that
A71: ( f . x = i & x = meet (g " {i}) & g " {i} <> {} ) by A11, A69;
consider Z being Subset-Family of (J . (In ((f . x),I))) such that
Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } and
A72: ( Z is open & Z is finite & not Z is empty ) and
A73: x = product ((Carrier J) +* ((f . x),(meet Z))) by A31, A69, A70, A71;
set W = meet Z;
take i ; :: thesis:
take J . (In ((f . x),I)) ; :: thesis:
take meet Z ; :: thesis:
thus ( i in I & meet Z is open & J . (In ((f . x),I)) = J . i & x = product ((Carrier J) +* (i,(meet Z))) ) by A71, A73, A72, TOPS_2:20; :: thesis:

end;

hence x in product_prebasis J by A69, WAYBEL18:def 2; :: thesis:

end;

suppose x = {} ; :: thesis:

hence x in product_prebasis J by Th56; :: thesis:

end;

hence X c= product_prebasis J by TARSKI:def 3; :: thesis:
for x being object holds
( x in meet X iff x in meet Y )

proof

let x be object ; :: thesis:

hereby :: thesis:

assume A74: x in meet X ; :: thesis:
for Sy being set st Sy in Y holds
x in Sy

proof

let Sy be set ; :: thesis:
assume A75: Sy in Y ; :: thesis:
then consider i being Element of I, B being Subset of (J . i) such that
A76: ( g . Sy = i & B is open & Sy = product ((Carrier J) +* (i,B)) ) by A7;
g . Sy in {i} by A76, TARSKI:def 1;
then A77: Sy in g " {i} by A75, FUNCT_2:38;
then meet (g " {i}) in X ;
then A78: x in meet (g " {i}) by A74, SETFAM_1:def 1;
meet (g " {i}) c= Sy by A77, SETFAM_1:3;
hence x in Sy by A78; :: thesis:

end;

hence x in meet Y by A3, SETFAM_1:def 1; :: thesis:

end;

assume A79: x in meet Y ; :: thesis:
for Sx being set st Sx in X holds
x in Sx

proof

let Sx be set ; :: thesis:
assume Sx in X ; :: thesis:
then consider i being Element of I such that
A80: ( Sx = meet (g " {i}) & g " {i} <> {} ) ;
for A being set st A in g " {i} holds
x in A by A79, SETFAM_1:def 1;
hence x in Sx by A80, SETFAM_1:def 1; :: thesis:

end;

hence x in meet X by A27, SETFAM_1:def 1; :: thesis:

end;

then A81: meet X = meet Y by TARSKI:2;
thus X is finite :: thesis:

proof

set S = { (g " {i}) where i is Element of I : i in rng g } ;
a82: { (g " {i}) where i is Element of I : i in rng g } is a_partition of Y by Th5;
defpred S₃[ object , object ] means ex M being set st
( $1 = M & $2 = meet M );
A83: for A being object st A in { (g " {i}) where i is Element of I : i in rng g } holds
ex B being object st
( B in X & S₃[A,B] )

proof

let A be object ; :: thesis:
assume A in { (g " {i}) where i is Element of I : i in rng g } ; :: thesis:
then consider i being Element of I such that
A84: ( A = g " {i} & i in rng g ) ;
take meet (g " {i}) ; :: thesis:
consider x being object such that
A85: ( x in Y & g . x = i ) by A84, FUNCT_2:11;
i in {i} by TARSKI:def 1;
then x in g " {i} by A85, FUNCT_2:38;
hence meet (g " {i}) in X ; :: thesis:
take g " {i} ; :: thesis:
thus ( A = g " {i} & meet (g " {i}) = meet (g " {i}) ) by A84; :: thesis:

end;

consider h being Function of { (g " {i}) where i is Element of I : i in rng g } ,X such that
A86: for A being object st A in { (g " {i}) where i is Element of I : i in rng g } holds
S₃[A,h . A] from FUNCT_2:sch 1(A83);
for B being object st B in X holds
ex A being object st
( A in { (g " {i}) where i is Element of I : i in rng g } & B = h . A )

proof

let B be object ; :: thesis:
assume B in X ; :: thesis:
then consider i being Element of I such that
A87: ( B = meet (g " {i}) & g " {i} <> {} ) ;
take g " {i} ; :: thesis:
consider x being object such that
A88: x in g " {i} by A87, XBOOLE_0:def 1;
( x in Y & g . x in {i} ) by A88, FUNCT_2:38;
then A90: g . x = i by TARSKI:def 1;
dom g = Y by FUNCT_2:def 1;
then i in rng g by A88, A90, FUNCT_1:def 3;
hence g " {i} in { (g " {i}) where i is Element of I : i in rng g } ; :: thesis:
then ex M being set st
( g " {i} = M & h . (g " {i}) = meet M ) by A86;
hence B = h . (g " {i}) by A87; :: thesis:

end;

then rng h = X by FUNCT_2:10;
hence X is finite by a82, A2; :: thesis:

end;

thus P = Intersect X by A4, A27, A81, SETFAM_1:def 9; :: thesis:
thus dom f = X by FUNCT_2:def 1; :: thesis:
set F = (Carrier J) +* (product_basis_selector (J,f));
for x being object holds
( x in meet X iff x in product ((Carrier J) +* (product_basis_selector (J,f))) )

proof

let x be object ; :: thesis:
A92: I = I \/ (rng f) by XBOOLE_1:12
.= (dom (Carrier J)) \/ (rng f) by PARTFUN1:def 2
.= (dom (Carrier J)) \/ (dom (product_basis_selector (J,f))) by PARTFUN1:def 2
.= dom ((Carrier J) +* (product_basis_selector (J,f))) by FUNCT_4:def 1 ;

hereby :: thesis:

assume A93: x in meet X ; :: thesis:
consider A0 being object such that
A94: A0 in X by A27, XBOOLE_0:def 1;
reconsider A0 = A0 as set by TARSKI:1;
consider i0 being Element of I such that
A95: ( f . A0 = i0 & A0 = meet (g " {i0}) & g " {i0} <> {} ) by A11, A94;
A0 <> {} by A3, A81, A94, SETFAM_1:4;
then consider Z0 being Subset-Family of (J . (In ((f . A0),I))) such that
Z0 = { ((proj (J,(In ((f . A0),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . A0)} } and
( Z0 is open & Z0 is finite & not Z0 is empty ) and
A96: A0 = product ((Carrier J) +* ((f . A0),(meet Z0))) by A31, A94, A95;
x in A0 by A93, A94, SETFAM_1:def 1;
then consider h being Function such that
A97: ( x = h & dom h = dom ((Carrier J) +* ((f . A0),(meet Z0))) ) and
A98: for y being object st y in dom ((Carrier J) +* ((f . A0),(meet Z0))) holds
h . y in ((Carrier J) +* ((f . A0),(meet Z0))) . y by A96, CARD_3:def 5;
A99: dom h = I by A97, PARTFUN1:def 2;
A100: dom h = dom ((Carrier J) +* (product_basis_selector (J,f))) by A92, A97, PARTFUN1:def 2;
for y being object st y in dom ((Carrier J) +* (product_basis_selector (J,f))) holds
h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y

proof

let y be object ; :: thesis:
assume y in dom ((Carrier J) +* (product_basis_selector (J,f))) ; :: thesis:
then reconsider i = y as Element of I by A92;
i in dom h by A99;
then A101: i in dom (Carrier J) by A97, FUNCT_7:30;

per cases ;

suppose A102: y in rng f ; :: thesis:

then y in dom (product_basis_selector (J,f)) by PARTFUN1:def 2;
then ((Carrier J) +* (product_basis_selector (J,f))) . y = (product_basis_selector (J,f)) . i by FUNCT_4:13;
then A103: ((Carrier J) +* (product_basis_selector (J,f))) . y = (proj (J,i)) .: ((f ") . i) by A102, Th54;
consider A being object such that
A104: ( A in X & f . A = i ) by A102, FUNCT_2:11;
reconsider A = A as set by TARSKI:1;
consider j being Element of I such that
A105: ( f . A = j & A = meet (g " {j}) & g " {j} <> {} ) by A11, A104;
A <> {} by A3, A81, A104, SETFAM_1:4;
then consider Z being Subset-Family of (J . (In ((f . A),I))) such that
Z = { ((proj (J,(In ((f . A),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . A)} } and
( Z is open & Z is finite & not Z is empty ) and
A106: A = product ((Carrier J) +* ((f . A),(meet Z))) by A31, A104, A105;
reconsider Z = Z as Subset-Family of (J . i) by A104;
a107: h in A by A93, A97, A104, SETFAM_1:def 1;
dom ((Carrier J) +* ((f . A),(meet Z))) = I by PARTFUN1:def 2;
then h . i in ((Carrier J) +* ((f . A),(meet Z))) . i by a107, A106, CARD_3:9;
then A108: h . i in meet Z by A104, A101, FUNCT_7:31;
ex z being object st
( z in dom (proj (J,i)) & z in meet (g " {i}) & (proj (J,i)) . z = h . i )

proof

end;

then h . i in (proj (J,i)) .: (meet (g " {i})) by FUNCT_1:def 6;
hence h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y by A103, A105, A12, A104, FUNCT_1:34; :: thesis:

end;

suppose not y in rng f ; :: thesis:

then not y in dom (product_basis_selector (J,f)) ;
then A114: ((Carrier J) +* (product_basis_selector (J,f))) . y = (Carrier J) . y by FUNCT_4:11;
reconsider Z0 = Z0 as Subset-Family of (J . i0) by A95;
meet Z0 c= the carrier of (J . i0) ;
then meet Z0 c= [#] (J . i0) by STRUCT_0:def 3;
then A115: meet Z0 c= (Carrier J) . i0 by PENCIL_3:7;
i0 in I ;
then i0 in dom (Carrier J) by PARTFUN1:def 2;
then A116: product ((Carrier J) +* (i0,(meet Z0))) c= product (Carrier J) by A115, Th39;
h in product ((Carrier J) +* (i0,(meet Z0))) by A95, A97, A98, CARD_3:9;
hence h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y by A114, A101, A116, CARD_3:9; :: thesis:

end;

hence x in product ((Carrier J) +* (product_basis_selector (J,f))) by A97, A100, CARD_3:def 5; :: thesis:

end;

assume x in product ((Carrier J) +* (product_basis_selector (J,f))) ; :: thesis:
then consider h being Function such that
A117: ( h = x & dom h = dom ((Carrier J) +* (product_basis_selector (J,f))) ) and
A118: for y being object st y in dom ((Carrier J) +* (product_basis_selector (J,f))) holds
h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y by CARD_3:def 5;
for A being set st A in X holds
h in A

proof

let A be set ; :: thesis:
assume A119: A in X ; :: thesis:
then consider i being Element of I such that
A120: ( f . A = i & A = meet (g " {i}) & g " {i} <> {} ) by A11;
A121: (f ") . i = A by A12, A119, A120, FUNCT_1:34;
A <> {} by A3, A81, A119, SETFAM_1:4;
then consider Z being Subset-Family of (J . (In ((f . A),I))) such that
A122: Z = { ((proj (J,(In ((f . A),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . A)} } and
( Z is open & Z is finite & not Z is empty ) and
A124: A = product ((Carrier J) +* ((f . A),(meet Z))) by A31, A119, A120;
A125: dom h = dom ((Carrier J) +* ((f . A),(meet Z))) by A92, A117, PARTFUN1:def 2;
for y being object st y in dom ((Carrier J) +* ((f . A),(meet Z))) holds
h . y in ((Carrier J) +* ((f . A),(meet Z))) . y

proof

let y be object ; :: thesis:
assume A126: y in dom ((Carrier J) +* ((f . A),(meet Z))) ; :: thesis:

per cases ;

suppose y <> i ; :: thesis:

then A127: ((Carrier J) +* ((f . A),(meet Z))) . y = (Carrier J) . y by A120, FUNCT_7:32;
A128: y in dom (Carrier J) by A126, FUNCT_7:30;
A129: h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y by A92, A118, A126;

per cases ;

suppose A130: y in rng f ; :: thesis:

then reconsider i0 = y as Element of I ;
y in dom (product_basis_selector (J,f)) by A130, PARTFUN1:def 2;
then ((Carrier J) +* (product_basis_selector (J,f))) . y = (product_basis_selector (J,f)) . i0 by FUNCT_4:13
.= (proj (J,i0)) .: ((f ") . i0) by A130, Th54 ;
then ((Carrier J) +* (product_basis_selector (J,f))) . y c= rng (proj (J,i0)) by RELAT_1:111;
then ((Carrier J) +* (product_basis_selector (J,f))) . y c= rng (proj ((Carrier J),i0)) by WAYBEL18:def 4;
then ((Carrier J) +* (product_basis_selector (J,f))) . y c= (Carrier J) . i0 by A128, YELLOW17:3;
hence h . y in ((Carrier J) +* ((f . A),(meet Z))) . y by A127, A129; :: thesis:

end;

suppose not y in rng f ; :: thesis:

then not y in dom (product_basis_selector (J,f)) ;
hence h . y in ((Carrier J) +* ((f . A),(meet Z))) . y by A127, A129, FUNCT_4:11; :: thesis:

end;

suppose A131: y = i ; :: thesis:

i in I ;
then a132: i in dom (Carrier J) by PARTFUN1:def 2;
A133: i in rng f by A12, A119, A120, FUNCT_1:def 3;
then i in dom (product_basis_selector (J,f)) by PARTFUN1:def 2;
then A134: ((Carrier J) +* (product_basis_selector (J,f))) . i = (product_basis_selector (J,f)) . i by FUNCT_4:13
.= (proj (J,i)) .: (meet (g " {i})) by A120, A121, A133, Th54 ;
reconsider G = g " {i} as Subset-Family of (product (Carrier J)) by XBOOLE_1:1;
h . i in (proj (J,i)) .: (meet (g " {i})) by A92, A118, A134;
then h . i in meet { ((proj (J,i)) .: B) where B is Subset of (product (Carrier J)) : B in G } by Th3, TARSKI:def 3;
hence h . y in ((Carrier J) +* ((f . A),(meet Z))) . y by A131, a132, FUNCT_7:31, A120, A122; :: thesis:

end;

hence h in A by A124, A125, CARD_3:9; :: thesis:

end;

hence x in meet X by A27, A117, SETFAM_1:def 1; :: thesis:

end;

hence P = product ((Carrier J) +* (product_basis_selector (J,f))) by A4, A81, TARSKI:2; :: thesis:

end;

suppose A136: Y is empty ; :: thesis:

reconsider f = the empty Function as I -valued one-to-one Function by XBOOLE_1:2, RELAT_1:38, RELAT_1:def 19;
take Y ; :: thesis:
take f ; :: thesis:
thus ( Y c= product_prebasis J & Y is finite & P = Intersect Y ) by A2; :: thesis:
thus dom f = Y by A136; :: thesis:
product_basis_selector (J,f) is empty ;
hence P = product ((Carrier J) +* (product_basis_selector (J,f))) by A2, A136, SETFAM_1:def 9; :: thesis:

end;

suppose ( not Y is empty & meet Y = {} ) ; :: thesis:

then A138: P = {} by A2, SETFAM_1:def 9;
set i = the Element of I;
set V = the empty Subset of (J . the Element of I);
a139: dom (Carrier J) = I by PARTFUN1:def 2;
then A140: product ((Carrier J) +* ( the Element of I, the empty Subset of (J . the Element of I))) = {} by Th36;
then product ((Carrier J) +* ( the Element of I, the empty Subset of (J . the Element of I))) in product_prebasis J by Th56;
then reconsider A = product ((Carrier J) +* ( the Element of I, the empty Subset of (J . the Element of I))) as Subset of (product (Carrier J)) ;
set X = {A};
set f = A .--> the Element of I;
take {A} ; :: thesis:
take A .--> the Element of I ; :: thesis:
thus ( {A} c= product_prebasis J & {A} is finite ) by A140, Th56, ZFMISC_1:31; :: thesis:
{} in {A} by A140, TARSKI:def 1;
then meet {A} = {} by SETFAM_1:4;
hence P = Intersect {A} by A138, SETFAM_1:def 9; :: thesis:
thus dom (A .--> the Element of I) = dom ({A} --> the Element of I) by FUNCOP_1:def 9
.= {A} ; :: thesis:
set F = (Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)));
ex j being object st
( j in dom ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) & ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) . j = {} )

proof

take the Element of I ; :: thesis:
the Element of I in (dom (Carrier J)) \/ (dom (product_basis_selector (J,(A .--> the Element of I)))) by a139, XBOOLE_1:7, TARSKI:def 3;
hence the Element of I in dom ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) by FUNCT_4:def 1; :: thesis:
the Element of I in { the Element of I} by TARSKI:def 1;
then the Element of I in rng ({A} --> the Element of I) by FUNCOP_1:8;
then A142: the Element of I in rng (A .--> the Element of I) by FUNCOP_1:def 9;
then the Element of I in dom (product_basis_selector (J,(A .--> the Element of I))) by PARTFUN1:def 2;
hence ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) . the Element of I = (product_basis_selector (J,(A .--> the Element of I))) . the Element of I by FUNCT_4:13
.= (proj (J, the Element of I)) .: (((A .--> the Element of I) ") . the Element of I) by A142, Th54
.= (proj (J, the Element of I)) .: (( the Element of I .--> A) . the Element of I) by NECKLACE:9
.= (proj (J, the Element of I)) .: A by FUNCOP_1:72
.= {} by A140 ;
:: thesis:

end;

then {} in rng ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) by FUNCT_1:def 3;
hence P = product ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) by A138, CARD_3:26; :: thesis:

end;