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

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

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

then
||.t.|| <= n * K
by Th16;
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;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

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