let n be Nat; :: thesis: for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1) holds
PP is open
let PP be Subset-Family of (TopSpaceMetr (Euclid n)); :: thesis: ( PP = product_prebasis ((Seg n) --> R^1) implies PP is open )
set J = (Seg n) --> R^1;
set C = Carrier ((Seg n) --> R^1);
set T = TopSpaceMetr (Euclid n);
set E = Euclid n;
assume A1: PP = product_prebasis ((Seg n) --> R^1) ; :: thesis: PP is open
let x be Subset of (TopSpaceMetr (Euclid n)); :: according to TOPS_2:def 1 :: thesis: ( not x in PP or x is open )
assume x in PP ; :: thesis: x is open
then consider i being set , R being TopStruct , V being Subset of R such that
A2: i in Seg n and
A3: V is open and
A4: R = ((Seg n) --> R^1) . i and
A5: x = product ((Carrier ((Seg n) --> R^1)) +* (i,V)) by A1, WAYBEL18:def 2;
A6: dom (Carrier ((Seg n) --> R^1)) = Seg n by PARTFUN1:def 2;

A7: now

let i be set ; :: thesis: for e, y being Point of (Euclid n)
for r being real number st y in Ball (e,r) holds
y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[))
let e, y be Point of (Euclid n); :: thesis: for r being real number st y in Ball (e,r) holds
y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[))
let r be real number ; :: thesis: ( y in Ball (e,r) implies y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) )
assume A8: y in Ball (e,r) ; :: thesis: y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[))
set O = ].((e . i) - r),((e . i) + r).[;
set G = (Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[);
A9: dom y = Seg n by FINSEQ_1:89;
A10: dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30;

now

let a be set ; :: thesis: ( a in dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) implies y . b₁ in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b₁ )
assume A11: a in dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) ; :: thesis: y . b₁ in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b₁

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

suppose A12: a = i ; :: thesis: y . b₁ in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b₁

A13: ( r is Real & e . i is Real & y . i is Real & (y . i) - (e . i) is Real ) by XREAL_0:def 1;
A14: y . i = (e . i) + ((y . i) - (e . i)) ;
A15: dom e = Seg n by FINSEQ_1:89;
dom (y - e) = (dom y) /\ (dom e) by VALUED_1:12;
then A16: (y - e) . i = (y . i) - (e . i) by A9, A15, A11, A12, A6, A10, VALUED_1:13;
abs ((y - e) . i) < r by A8, Th10;
then y . i in ].((e . i) - r),((e . i) + r).[ by A16, A13, A14, FCONT_3:3;
hence y . a in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a by A12, A10, A11, FUNCT_7:31; :: thesis: verum

end;

suppose a <> i ; :: thesis: y . b₁ in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b₁

then A17: ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a = (Carrier ((Seg n) --> R^1)) . a by FUNCT_7:32;
A18: ex R being 1-sorted st
( R = ((Seg n) --> R^1) . a & (Carrier ((Seg n) --> R^1)) . a = the carrier of R ) by A11, A10, A6, PRALG_1:def 13;
y . a in REAL by XREAL_0:def 1;
hence y . a in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a by A17, A11, A10, A6, A18, FUNCOP_1:7; :: thesis: verum

end;

end;

end;

hence y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) by A10, A6, A9, CARD_3:9; :: thesis: verum

end;

set F = (Carrier ((Seg n) --> R^1)) +* (i,V);
A19: R = R^1 by A2, A4, FUNCOP_1:7;
for e being Element of (Euclid n) st e in x holds
ex r being Real st
( r > 0 & Ball (e,r) c= x )

proof

let e be Element of (Euclid n); :: thesis: ( e in x implies ex r being Real st
( r > 0 & Ball (e,r) c= x ) )
assume A20: e in x ; :: thesis: ex r being Real st
( r > 0 & Ball (e,r) c= x )
A21: dom ((Carrier ((Seg n) --> R^1)) +* (i,V)) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30;
then A22: e . i in ((Carrier ((Seg n) --> R^1)) +* (i,V)) . i by A2, A6, A20, A5, CARD_3:9;
A23: ((Carrier ((Seg n) --> R^1)) +* (i,V)) . i = V by A2, A6, FUNCT_7:31;
then consider r being Real such that
A24: r > 0 and
A25: ].((e . i) - r),((e . i) + r).[ c= V by A3, A19, A22, FRECHET:8;
take r ; :: thesis: ( r > 0 & Ball (e,r) c= x )
thus r > 0 by A24; :: thesis: Ball (e,r) c= x
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Ball (e,r) or y in x )
assume A26: y in Ball (e,r) ; :: thesis: y in x
then reconsider y = y as Point of (Euclid n) ;
set O = ].((e . i) - r),((e . i) + r).[;
set G = (Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[);
A27: dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30;
A28: y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) by A26, A7;

now

let a be set ; :: thesis: ( a in dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) implies ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b₁ c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . b₁ )
assume A29: a in dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) ; :: thesis: ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b₁ c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . b₁

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

suppose a = i ; :: thesis: ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b₁ c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . b₁

hence ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . a by A25, A23, A27, A29, FUNCT_7:31; :: thesis: verum

end;

suppose a <> i ; :: thesis: ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b₁ c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . b₁

then ( ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a = (Carrier ((Seg n) --> R^1)) . a & ((Carrier ((Seg n) --> R^1)) +* (i,V)) . a = (Carrier ((Seg n) --> R^1)) . a ) by FUNCT_7:32;
hence ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . a ; :: thesis: verum

end;

end;

end;

then product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) c= product ((Carrier ((Seg n) --> R^1)) +* (i,V)) by A21, CARD_3:27, FUNCT_7:30;
hence y in x by A28, A5; :: thesis: verum

end;

then x in the topology of (TopSpaceMetr (Euclid n)) by PCOMPS_1:def 4;
hence x is open by PRE_TOPC:def 2; :: thesis: verum