let m be non zero Element of NAT ; :: thesis: for x being Element of REAL m
for Z being Subset of (REAL m)
for i being Nat st Z is open & x in Z & 1 <= i & i <= m holds
ex N being Neighbourhood of (proj (i,m)) . x st
for z being Element of REAL st z in N holds
(reproj (i,x)) . z in Z
let x be Element of REAL m; :: thesis: for Z being Subset of (REAL m)
for i being Nat st Z is open & x in Z & 1 <= i & i <= m holds
ex N being Neighbourhood of (proj (i,m)) . x st
for z being Element of REAL st z in N holds
(reproj (i,x)) . z in Z
let Z be Subset of (REAL m); :: thesis: for i being Nat st Z is open & x in Z & 1 <= i & i <= m holds
ex N being Neighbourhood of (proj (i,m)) . x st
for z being Element of REAL st z in N holds
(reproj (i,x)) . z in Z
let i be Nat; :: thesis: ( Z is open & x in Z & 1 <= i & i <= m implies ex N being Neighbourhood of (proj (i,m)) . x st
for z being Element of REAL st z in N holds
(reproj (i,x)) . z in Z )
assume that
A1: ( Z is open & x in Z ) and
A2: ( 1 <= i & i <= m ) ; :: thesis: ex N being Neighbourhood of (proj (i,m)) . x st
for z being Element of REAL st z in N holds
(reproj (i,x)) . z in Z
consider r being Real such that
A3: ( 0 < r & { y where y is Element of REAL m : |.(y - x).| < r } c= Z ) by A1, PDIFF_7:31;
set N = ].(((proj (i,m)) . x) - r),(((proj (i,m)) . x) + r).[;
reconsider N = ].(((proj (i,m)) . x) - r),(((proj (i,m)) . x) + r).[ as Neighbourhood of (proj (i,m)) . x by A3, RCOMP_1:def 6;
take N ; :: thesis: for z being Element of REAL st z in N holds
(reproj (i,x)) . z in Z
let z be Element of REAL ; :: thesis: ( z in N implies (reproj (i,x)) . z in Z )
assume z in N ; :: thesis: (reproj (i,x)) . z in Z
then A4: |.(z - ((proj (i,m)) . x)).| < r by RCOMP_1:1;
|.(((reproj (i,x)) . z) - x).| = |.((reproj (i,(0* m))) . (z - ((proj (i,m)) . x))).| by PDIFF_7:6
.= |.(z - ((proj (i,m)) . x)).| by A2, Th11 ;
then (reproj (i,x)) . z in { y where y is Element of REAL m : |.(y - x).| < r } by A4;
hence (reproj (i,x)) . z in Z by A3; :: thesis: verum