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 A2: 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
A16: i in Seg n and
A17: V is open and
A18: R = ((Seg n) --> R^1 ) . i and
A19: x = product ((Carrier ((Seg n) --> R^1 )) +* i,V) by A2, WAYBEL18:def 2;
n <> 0 by A16;
then reconsider S = Seg n as non empty finite set ;
A3: dom (Carrier ((Seg n) --> R^1 )) = Seg n by PARTFUN1:def 4;

A4: 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 A5: 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).[;
A6: dom y = Seg n by EUCLID:3;
A7: dom ((Carrier ((Seg n) --> R^1 )) +* i,].((e . i) - r),((e . i) + r).[) = dom (Carrier ((Seg n) --> R^1 )) by FUNCT_7:32;

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 A8: 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 A9: a = i ; :: thesis: y . b₁ in ((Carrier ((Seg n) --> R^1 )) +* i,].((e . i) - r),((e . i) + r).[) . b₁

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

end;

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

then A14: ((Carrier ((Seg n) --> R^1 )) +* i,].((e . i) - r),((e . i) + r).[) . a = (Carrier ((Seg n) --> R^1 )) . a by FUNCT_7:34;
A15: ex R being 1-sorted st
( R = ((Seg n) --> R^1 ) . a & (Carrier ((Seg n) --> R^1 )) . a = the carrier of R ) by A8, A7, A3, 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 A14, A8, A7, A3, A15, FUNCOP_1:13; :: thesis: verum

end;

end;

end;

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

end;

set F = (Carrier ((Seg n) --> R^1 )) +* i,V;
A20: R = R^1 by A16, A18, FUNCOP_1:13;
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 A21: e in x ; :: thesis: ex r being Real st
( r > 0 & Ball e,r c= x )
A22: dom ((Carrier ((Seg n) --> R^1 )) +* i,V) = dom (Carrier ((Seg n) --> R^1 )) by FUNCT_7:32;
then A23: e . i in ((Carrier ((Seg n) --> R^1 )) +* i,V) . i by A16, A3, A21, A19, CARD_3:18;
A24: ((Carrier ((Seg n) --> R^1 )) +* i,V) . i = V by A16, A3, FUNCT_7:33;
then consider r being Real such that
A25: r > 0 and
A26: ].((e . i) - r),((e . i) + r).[ c= V by A17, A20, A23, FRECHET:8;
take r ; :: thesis: ( r > 0 & Ball e,r c= x )
thus r > 0 by A25; :: 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 A27: 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).[;
A28: dom ((Carrier ((Seg n) --> R^1 )) +* i,].((e . i) - r),((e . i) + r).[) = dom (Carrier ((Seg n) --> R^1 )) by FUNCT_7:32;
A29: y in product ((Carrier ((Seg n) --> R^1 )) +* i,].((e . i) - r),((e . i) + r).[) by A27, A4;

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 A30: 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 A26, A24, A28, A30, FUNCT_7:33; :: 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:34;
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 A22, CARD_3:38, FUNCT_7:32;
hence y in x by A29, A19; :: thesis: verum

end;

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