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

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