let n be non zero Element of NAT ; :: thesis: for x being Point of (REAL-NS n)
for i being Nat st 1 <= i & i <= n holds
||.((Proj (i,n)) . x).|| <= ||.x.||
let x be Point of (REAL-NS n); :: thesis: for i being Nat st 1 <= i & i <= n holds
||.((Proj (i,n)) . x).|| <= ||.x.||
let i be Nat; :: thesis: ( 1 <= i & i <= n implies ||.((Proj (i,n)) . x).|| <= ||.x.|| )
assume A1: ( 1 <= i & i <= n ) ; :: thesis: ||.((Proj (i,n)) . x).|| <= ||.x.||
reconsider y = x as Element of REAL n by REAL_NS1:def 4;
A2: ||.x.|| = |.y.| by REAL_NS1:1;
(Proj (i,n)) . x = <*((proj (i,n)) . x)*> by PDIFF_1:def 4
.= <*(y . i)*> by PDIFF_1:def 1 ;
then A3: ||.((Proj (i,n)) . x).|| = |.(y . i).| by Th2;
reconsider p = y as Element of (TOP-REAL n) by EUCLID:22;
A4: i in Seg n by A1;
then A5: |.(p /. i).| <= |.y.| by Th1;
i in dom y by A4, FINSEQ_1:89;
hence ||.((Proj (i,n)) . x).|| <= ||.x.|| by A2, A3, A5, PARTFUN1:def 6; :: thesis: verum