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;

now :: thesis: for i being Element of NAT st 1 <= i & i <= m + 1 holds
|.(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;

then |.s0.| <= n * K by A2, Th15;
hence ||.s.|| <= n * K by REAL_NS1:1; :: thesis: verum