let m be Nat; :: thesis: for nx being Point of (REAL-NS m)
for Z being Subset of (REAL-NS m)
for i being Nat st Z is open & nx in Z & 1 <= i & i <= m holds
ex N being Neighbourhood of (Proj (i,m)) . nx st
for z being Point of (REAL-NS 1) st z in N holds
(reproj (i,nx)) . z in Z
let nx be Point of (REAL-NS m); :: thesis: for Z being Subset of (REAL-NS m)
for i being Nat st Z is open & nx in Z & 1 <= i & i <= m holds
ex N being Neighbourhood of (Proj (i,m)) . nx st
for z being Point of (REAL-NS 1) st z in N holds
(reproj (i,nx)) . z in Z
let Z be Subset of (REAL-NS m); :: thesis: for i being Nat st Z is open & nx in Z & 1 <= i & i <= m holds
ex N being Neighbourhood of (Proj (i,m)) . nx st
for z being Point of (REAL-NS 1) st z in N holds
(reproj (i,nx)) . z in Z
let i be Nat; :: thesis: ( Z is open & nx in Z & 1 <= i & i <= m implies ex N being Neighbourhood of (Proj (i,m)) . nx st
for z being Point of (REAL-NS 1) st z in N holds
(reproj (i,nx)) . z in Z )
assume that
A1: Z is open and
A2: nx in Z and
A3: ( 1 <= i & i <= m ) ; :: thesis: ex N being Neighbourhood of (Proj (i,m)) . nx st
for z being Point of (REAL-NS 1) st z in N holds
(reproj (i,nx)) . z in Z
consider r being Real such that
A4: ( 0 < r & { y where y is Point of (REAL-NS m) : ||.(y - nx).|| < r } c= Z ) by A1, A2, NDIFF_1:3;
set N = { y where y is Point of (REAL-NS 1) : ||.(y - ((Proj (i,m)) . nx)).|| < r } ;
reconsider N = { y where y is Point of (REAL-NS 1) : ||.(y - ((Proj (i,m)) . nx)).|| < r } as Neighbourhood of (Proj (i,m)) . nx by A4, NFCONT_1:3;
take N ; :: thesis: for z being Point of (REAL-NS 1) st z in N holds
(reproj (i,nx)) . z in Z
let z be Point of (REAL-NS 1); :: thesis: ( z in N implies (reproj (i,nx)) . z in Z )
assume z in N ; :: thesis: (reproj (i,nx)) . z in Z
then A5: ex y being Point of (REAL-NS 1) st
( y = z & ||.(y - ((Proj (i,m)) . nx)).|| < r ) ;
||.(((reproj (i,nx)) . z) - nx).|| = ||.((reproj (i,(0. (REAL-NS m)))) . (z - ((Proj (i,m)) . nx))).|| by Th7
.= ||.(z - ((Proj (i,m)) . nx)).|| by A3, Th5 ;
then (reproj (i,nx)) . z in { y where y is Point of (REAL-NS m) : ||.(y - nx).|| < r } by A5;
hence (reproj (i,nx)) . z in Z by A4; :: thesis: verum