let K be Real; :: thesis: for n being non zero Element of NAT

for s being Element of (REAL-NS n) st ( for i being Element of NAT st 1 <= i & i <= n holds

||.((Proj (i,n)) . s).|| <= K ) holds

||.s.|| <= n * K

let n be non zero Element of NAT ; :: thesis: for s being Element of (REAL-NS n) st ( for i being Element of NAT st 1 <= i & i <= n holds

||.((Proj (i,n)) . s).|| <= K ) holds

||.s.|| <= n * K

let s be Element of (REAL-NS n); :: thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds

||.((Proj (i,n)) . s).|| <= K ) implies ||.s.|| <= n * K )

assume A1: for i being Element of NAT st 1 <= i & i <= n holds

||.((Proj (i,n)) . s).|| <= K ; :: thesis: ||.s.|| <= n * K

consider m being Nat such that

A2: n = m + 1 by NAT_1:6;

reconsider m = m as Element of NAT by ORDINAL1:def 12;

reconsider s0 = s as Element of REAL n by REAL_NS1:def 4;

hence ||.s.|| <= n * K by REAL_NS1:1; :: thesis: verum

for s being Element of (REAL-NS n) st ( for i being Element of NAT st 1 <= i & i <= n holds

||.((Proj (i,n)) . s).|| <= K ) holds

||.s.|| <= n * K

let n be non zero Element of NAT ; :: thesis: for s being Element of (REAL-NS n) st ( for i being Element of NAT st 1 <= i & i <= n holds

||.((Proj (i,n)) . s).|| <= K ) holds

||.s.|| <= n * K

let s be Element of (REAL-NS n); :: thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds

||.((Proj (i,n)) . s).|| <= K ) implies ||.s.|| <= n * K )

assume A1: for i being Element of NAT st 1 <= i & i <= n holds

||.((Proj (i,n)) . s).|| <= K ; :: thesis: ||.s.|| <= n * K

consider m being Nat such that

A2: n = m + 1 by NAT_1:6;

reconsider m = m as Element of NAT by ORDINAL1:def 12;

reconsider s0 = s as Element of REAL n by REAL_NS1:def 4;

now :: thesis: for i being Element of NAT st 1 <= i & i <= m + 1 holds

|.(s0 . i).| <= K

then
|.s0.| <= n * K
by A2, Th15;|.(s0 . i).| <= K

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= m + 1 implies |.(s0 . i).| <= K )

assume ( 1 <= i & i <= m + 1 ) ; :: thesis: |.(s0 . i).| <= K

then A3: ||.((Proj (i,n)) . s).|| <= K by A2, A1;

(Proj (i,n)) . s = <*((proj (i,n)) . s0)*> by PDIFF_1:def 4

.= <*(s0 . i)*> by PDIFF_1:def 1 ;

hence |.(s0 . i).| <= K by A3, Th2; :: thesis: verum

end;assume ( 1 <= i & i <= m + 1 ) ; :: thesis: |.(s0 . i).| <= K

then A3: ||.((Proj (i,n)) . s).|| <= K by A2, A1;

(Proj (i,n)) . s = <*((proj (i,n)) . s0)*> by PDIFF_1:def 4

.= <*(s0 . i)*> by PDIFF_1:def 1 ;

hence |.(s0 . i).| <= K by A3, Th2; :: thesis: verum

hence ||.s.|| <= n * K by REAL_NS1:1; :: thesis: verum