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