let G be RealNormSpace-Sequence; :: thesis: for i being Element of dom G
for x being Point of (product G)
for Z being Subset of (product G) st Z is open & x in Z holds
ex N being Neighbourhood of (proj i) . x st
for z being Point of (G . i) st z in N holds
(reproj (i,x)) . z in Z
let i be Element of dom G; :: thesis: for x being Point of (product G)
for Z being Subset of (product G) st Z is open & x in Z holds
ex N being Neighbourhood of (proj i) . x st
for z being Point of (G . i) st z in N holds
(reproj (i,x)) . z in Z
let x be Point of (product G); :: thesis: for Z being Subset of (product G) st Z is open & x in Z holds
ex N being Neighbourhood of (proj i) . x st
for z being Point of (G . i) st z in N holds
(reproj (i,x)) . z in Z
let Z be Subset of (product G); :: thesis: ( Z is open & x in Z implies ex N being Neighbourhood of (proj i) . x st
for z being Point of (G . i) st z in N holds
(reproj (i,x)) . z in Z )
assume ( Z is open & x in Z ) ; :: thesis: ex N being Neighbourhood of (proj i) . x st
for z being Point of (G . i) st z in N holds
(reproj (i,x)) . z in Z
then consider r being Real such that
A1: ( 0 < r & { y where y is Point of (product G) : ||.(y - x).|| < r } c= Z ) by NDIFF_1:3;
set N = { y where y is Point of (G . i) : ||.(y - ((proj i) . x)).|| < r } ;
reconsider N = { y where y is Point of (G . i) : ||.(y - ((proj i) . x)).|| < r } as Neighbourhood of (proj i) . x by A1, NFCONT_1:3;
take N ; :: thesis: for z being Point of (G . i) st z in N holds
(reproj (i,x)) . z in Z
thus for z being Point of (G . i) st z in N holds
(reproj (i,x)) . z in Z :: thesis: verum

proof

let z be Point of (G . i); :: thesis: ( z in N implies (reproj (i,x)) . z in Z )
assume z in N ; :: thesis: (reproj (i,x)) . z in Z
then A2: ex y being Point of (G . i) st
( y = z & ||.(y - ((proj i) . x)).|| < r ) ;
||.(((reproj (i,x)) . z) - x).|| = ||.((reproj (i,(0. (product G)))) . (z - ((proj i) . x))).|| by Th22
.= ||.(z - ((proj i) . x)).|| by Th21 ;
then (reproj (i,x)) . z in { y where y is Point of (product G) : ||.(y - x).|| < r } by A2;
hence (reproj (i,x)) . z in Z by A1; :: thesis: verum

end;