let K be Real; :: thesis: for n being non zero Element of NAT
for s being Element of REAL 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 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 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
reconsider t = s as Element of (REAL-NS n) by REAL_NS1:def 4;
for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . t).|| <= K

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= n implies ||.((Proj (i,n)) . t).|| <= K )
assume ( 1 <= i & i <= n ) ; :: thesis: ||.((Proj (i,n)) . t).|| <= K
then |.((proj (i,n)) . t).| <= K by A1;
hence ||.((Proj (i,n)) . t).|| <= K by Th4; :: thesis: verum

end;

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