let K be Real; :: thesis: for n being non zero Element of NAT
for s being Element of () st ( for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . s).|| <= K ) holds
<= n * K

let n be non zero Element of NAT ; :: thesis: for s being Element of () st ( for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . s).|| <= K ) holds
<= n * K

let s be Element of (); :: thesis: ( ( for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . s).|| <= K ) implies <= n * K )

assume A1: for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . s).|| <= K ; :: thesis: <= 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 ; :: thesis: verum
end;
then |.s0.| <= n * K by ;
hence ||.s.|| <= n * K by REAL_NS1:1; :: thesis: verum