theorem Th23: :: NDIFF_5:23

for G being RealNormSpace-Sequence
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