let n be Nat; :: thesis: ( n <> 0 implies for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1 ) holds
PP is quasi_prebasis )
assume A1: n <> 0 ; :: thesis: for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1 ) holds
PP is quasi_prebasis
set E = Euclid n;
set T = TopSpaceMetr (Euclid n);
let PP be Subset-Family of (TopSpaceMetr (Euclid n)); :: thesis: ( PP = product_prebasis ((Seg n) --> R^1 ) implies PP is quasi_prebasis )
set J = (Seg n) --> R^1 ;
set C = Carrier ((Seg n) --> R^1 );
set S = Seg n;
reconsider S = Seg n as non empty finite set by A1;
assume A2: PP = product_prebasis ((Seg n) --> R^1 ) ; :: thesis: PP is quasi_prebasis
A3: REAL n = Funcs (Seg n),REAL by FINSEQ_2:111;
A4: dom (Carrier ((Seg n) --> R^1 )) = Seg n by PARTFUN1:def 4;
A5: Funcs (Seg n),REAL = product (Carrier ((Seg n) --> R^1 )) by Th25;
defpred S₁[ set , set ] means ex e being Point of (Euclid n) st
( e = $1 & $2 = OpenHypercubes e );
A6: for i being Element of (TopSpaceMetr (Euclid n)) ex j being set st S₁[i,j]

proof

let i be Element of (TopSpaceMetr (Euclid n)); :: thesis: ex j being set st S₁[i,j]
reconsider j = i as Point of (Euclid n) ;
take OpenHypercubes j ; :: thesis: S₁[i, OpenHypercubes j]
take j ; :: thesis: ( j = i & OpenHypercubes j = OpenHypercubes j )
thus ( j = i & OpenHypercubes j = OpenHypercubes j ) ; :: thesis: verum

end;

consider NS being ManySortedSet of (TopSpaceMetr (Euclid n)) such that
A7: for x being Point of (TopSpaceMetr (Euclid n)) holds S₁[x,NS . x] from PBOOLE:sch 6(A6);

now

let x be Point of (TopSpaceMetr (Euclid n)); :: thesis: NS . x is Basis of x
reconsider y = x as Point of (Euclid n) ;
S₁[y,NS . y] by A7;
hence NS . x is Basis of x ; :: thesis: verum

end;

then reconsider NS = NS as Neighborhood_System of TopSpaceMetr (Euclid n) by TOPGEN_2:def 3;
take B = Union NS; :: according to CANTOR_1:def 5 :: thesis: B c= FinMeetCl PP
let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in B or b in FinMeetCl PP )
assume b in B ; :: thesis: b in FinMeetCl PP
then consider Z being set such that
A8: b in Z and
A9: Z in rng NS by TARSKI:def 4;
consider x being set such that
A10: x in dom NS and
A11: NS . x = Z by A9, FUNCT_1:def 5;
reconsider x = x as Point of (Euclid n) by A10, PARTFUN1:def 4;
A12: dom x = Seg n by EUCLID:3;
S₁[x,NS . x] by A7;
then consider m being non zero Element of NAT such that
A13: b = OpenHypercube x,(1 / m) by A8, A11;
deffunc H₂( set ) -> set = product ((Carrier ((Seg n) --> R^1 )) +* $1,(R^1 ].((x . $1) - (1 / m)),((x . $1) + (1 / m)).[));
defpred S₂[ set ] means verum;
set Y = { H₂(q) where q is Element of S : S₂[q] } ;
A14: { H₂(q) where q is Element of S : S₂[q] } is finite from PRE_CIRC:sch 1();
{ H₂(q) where q is Element of S : S₂[q] } c= bool the carrier of (TopSpaceMetr (Euclid n))

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in { H₂(q) where q is Element of S : S₂[q] } or s in bool the carrier of (TopSpaceMetr (Euclid n)) )
assume s in { H₂(q) where q is Element of S : S₂[q] } ; :: thesis: s in bool the carrier of (TopSpaceMetr (Euclid n))
then consider q being Element of S such that
A15: s = H₂(q) ;
H₂(q) c= the carrier of (TopSpaceMetr (Euclid n))

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in H₂(q) or z in the carrier of (TopSpaceMetr (Euclid n)) )
set f = (Carrier ((Seg n) --> R^1 )) +* q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[);
assume z in H₂(q) ; :: thesis: z in the carrier of (TopSpaceMetr (Euclid n))
then consider g being Function such that
A16: z = g and
A17: dom g = dom ((Carrier ((Seg n) --> R^1 )) +* q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[)) and
A18: for d being set st d in dom ((Carrier ((Seg n) --> R^1 )) +* q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[)) holds
g . d in ((Carrier ((Seg n) --> R^1 )) +* q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[)) . d by CARD_3:def 5;
A19: dom ((Carrier ((Seg n) --> R^1 )) +* q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[)) = dom (Carrier ((Seg n) --> R^1 )) by FUNCT_7:32;
then reconsider g = g as FinSequence by A4, A17, FINSEQ_1:def 2;
rng g c= REAL

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in rng g or b in REAL )
assume b in rng g ; :: thesis: b in REAL
then consider a being set such that
A20: a in dom g and
A21: g . a = b by FUNCT_1:def 5;
A22: g . a in ((Carrier ((Seg n) --> R^1 )) +* q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[)) . a by A17, A18, A20;

per cases ( a = q or a <> q ) ;

suppose a = q ; :: thesis: b in REAL

then ((Carrier ((Seg n) --> R^1 )) +* q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[)) . a = R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[ by A17, A19, A20, FUNCT_7:33;
hence b in REAL by A21, A22; :: thesis: verum

end;

suppose a <> q ; :: thesis: b in REAL

then A23: ((Carrier ((Seg n) --> R^1 )) +* q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[)) . a = (Carrier ((Seg n) --> R^1 )) . a by FUNCT_7:34;
ex R being 1-sorted st
( R = ((Seg n) --> R^1 ) . a & (Carrier ((Seg n) --> R^1 )) . a = the carrier of R ) by A20, A17, A19, A4, PRALG_1:def 13;
hence b in REAL by A21, A22, A23, A20, A17, A19, A4, FUNCOP_1:13; :: thesis: verum

end;

end;

end;

then g is FinSequence of REAL by FINSEQ_1:def 4;
then A24: g is Element of REAL * by FINSEQ_1:def 11;
n in NAT by ORDINAL1:def 13;
then len g = n by A4, A17, A19, FINSEQ_1:def 3;
hence z in the carrier of (TopSpaceMetr (Euclid n)) by A16, A24; :: thesis: verum

end;

hence s in bool the carrier of (TopSpaceMetr (Euclid n)) by A15, ZFMISC_1:def 1; :: thesis: verum

end;

then reconsider Y = { H₂(q) where q is Element of S : S₂[q] } as Subset-Family of (TopSpaceMetr (Euclid n)) ;
A25: Y c= PP

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Y or z in PP )
assume A26: z in Y ; :: thesis: z in PP
then consider i being Element of S such that
A27: z = H₂(i) ;
((Seg n) --> R^1 ) . i = R^1 by FUNCOP_1:13;
hence z in PP by A2, A5, A26, A3, A27, WAYBEL18:def 2; :: thesis: verum

end;

consider N being set such that
A28: N in S by XBOOLE_0:def 1;
A29: H₂(N) in Y by A28;
then A30: Intersect Y = meet Y by SETFAM_1:def 10;
A31: dom (Intervals x,(1 / m)) = dom x by Def3;

A32: now

let i be Element of S; :: thesis: product (Intervals x,(1 / m)) c= product ((Carrier ((Seg n) --> R^1 )) +* i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))
set f = (Carrier ((Seg n) --> R^1 )) +* i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[);
thus product (Intervals x,(1 / m)) c= product ((Carrier ((Seg n) --> R^1 )) +* i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)) :: thesis: verum

proof

let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in product (Intervals x,(1 / m)) or d in product ((Carrier ((Seg n) --> R^1 )) +* i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)) )
assume d in product (Intervals x,(1 / m)) ; :: thesis: d in product ((Carrier ((Seg n) --> R^1 )) +* i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))
then consider d1 being Function such that
A33: d = d1 and
A34: dom d1 = dom (Intervals x,(1 / m)) and
A35: for a being set st a in dom (Intervals x,(1 / m)) holds
d1 . a in (Intervals x,(1 / m)) . a by CARD_3:def 5;
A36: dom ((Carrier ((Seg n) --> R^1 )) +* i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)) = dom (Carrier ((Seg n) --> R^1 )) by FUNCT_7:32;

now

let k be set ; :: thesis: ( k in dom ((Carrier ((Seg n) --> R^1 )) +* i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)) implies d1 . b₁ in ((Carrier ((Seg n) --> R^1 )) +* i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)) . b₁ )
assume A37: k in dom ((Carrier ((Seg n) --> R^1 )) +* i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)) ; :: thesis: d1 . b₁ in ((Carrier ((Seg n) --> R^1 )) +* i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)) . b₁
then A38: (Intervals x,(1 / m)) . k = ].((x . k) - (1 / m)),((x . k) + (1 / m)).[ by A4, A36, A12, Def3;
A39: d1 . k in (Intervals x,(1 / m)) . k by A35, A4, A31, A12, A36, A37;

per cases ( k = i or k <> i ) ;

suppose k = i ; :: thesis: d1 . b₁ in ((Carrier ((Seg n) --> R^1 )) +* i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)) . b₁

hence d1 . k in ((Carrier ((Seg n) --> R^1 )) +* i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)) . k by A38, A39, A37, A36, FUNCT_7:33; :: thesis: verum

end;

suppose k <> i ; :: thesis: d1 . b₁ in ((Carrier ((Seg n) --> R^1 )) +* i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)) . b₁

then A40: ((Carrier ((Seg n) --> R^1 )) +* i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)) . k = (Carrier ((Seg n) --> R^1 )) . k by FUNCT_7:34;
A41: ex R being 1-sorted st
( R = ((Seg n) --> R^1 ) . k & (Carrier ((Seg n) --> R^1 )) . k = the carrier of R ) by A37, A36, A4, PRALG_1:def 13;
d1 . k in REAL by A38, A39;
hence d1 . k in ((Carrier ((Seg n) --> R^1 )) +* i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)) . k by A40, A41, A37, A36, A4, FUNCOP_1:13; :: thesis: verum

end;

end;

end;

hence d in product ((Carrier ((Seg n) --> R^1 )) +* i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)) by A33, A4, A34, A31, A12, A36, CARD_3:18; :: thesis: verum

end;

end;

b = Intersect Y

proof

now

let M be set ; :: thesis: ( M in Y implies b c= M )
assume M in Y ; :: thesis: b c= M
then ex i being Element of S st M = H₂(i) ;
hence b c= M by A13, A32; :: thesis: verum

end;

hence b c= Intersect Y by A30, A29, SETFAM_1:6; :: according to XBOOLE_0:def 10 :: thesis: Intersect Y c= b
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in Intersect Y or q in b )
assume A42: q in Intersect Y ; :: thesis: q in b
reconsider q = q as Function by A42;
A43: dom q = Seg n by A42, EUCLID:3;

now

let a be set ; :: thesis: ( a in dom (Intervals x,(1 / m)) implies q . a in (Intervals x,(1 / m)) . a )
assume A44: a in dom (Intervals x,(1 / m)) ; :: thesis: q . a in (Intervals x,(1 / m)) . a
A45: (Intervals x,(1 / m)) . a = ].((x . a) - (1 / m)),((x . a) + (1 / m)).[ by A44, A31, Def3;
set f = (Carrier ((Seg n) --> R^1 )) +* a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[);
H₂(a) in Y by A44, A31, A12;
then A46: q in H₂(a) by A42, SETFAM_1:58;
then A47: dom q = dom ((Carrier ((Seg n) --> R^1 )) +* a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[)) by CARD_3:18;
then A48: q . a in ((Carrier ((Seg n) --> R^1 )) +* a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[)) . a by A43, A44, A31, A12, A46, CARD_3:18;
dom ((Carrier ((Seg n) --> R^1 )) +* a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[)) = dom (Carrier ((Seg n) --> R^1 )) by FUNCT_7:32;
hence q . a in (Intervals x,(1 / m)) . a by A45, A48, A43, A44, A31, A12, A47, FUNCT_7:33; :: thesis: verum

end;

hence q in b by A13, A43, A31, A12, CARD_3:18; :: thesis: verum

end;

hence b in FinMeetCl PP by A25, A14, CANTOR_1:def 4; :: thesis: verum