let K be Real; :: thesis: for n being Nat

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

|.(s . i).| <= K ) holds

|.s.| <= n * K

defpred S_{1}[ Nat] means for s being Element of REAL $1 st ( for i being Element of NAT st 1 <= i & i <= $1 holds

|.(s . i).| <= K ) holds

|.s.| <= $1 * K;

A1: S_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A1, A2); :: thesis: verum

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

|.(s . i).| <= K ) holds

|.s.| <= n * K

defpred S

|.(s . i).| <= K ) holds

|.s.| <= $1 * K;

A1: S

proof

A2:
for n being Nat st S
let s be Element of REAL 0; :: thesis: ( ( for i being Element of NAT st 1 <= i & i <= 0 holds

|.(s . i).| <= K ) implies |.s.| <= 0 * K )

s = 0* 0 ;

hence ( ( for i being Element of NAT st 1 <= i & i <= 0 holds

|.(s . i).| <= K ) implies |.s.| <= 0 * K ) by EUCLID:7; :: thesis: verum

end;|.(s . i).| <= K ) implies |.s.| <= 0 * K )

s = 0* 0 ;

hence ( ( for i being Element of NAT st 1 <= i & i <= 0 holds

|.(s . i).| <= K ) implies |.s.| <= 0 * K ) by EUCLID:7; :: thesis: verum

S

proof

thus
for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A3: S_{1}[n]
; :: thesis: S_{1}[n + 1]

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

|.(s . i).| <= K ) implies |.s.| <= (n + 1) * K )

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

|.(s . i).| <= K ; :: thesis: |.s.| <= (n + 1) * K

set sn = s | n;

len s = n + 1 by CARD_1:def 7;

then len (s | n) = n by FINSEQ_3:53;

then reconsider sn = s | n as Element of REAL n by FINSEQ_2:92;

( 1 <= n + 1 & n + 1 <= n + 1 ) by NAT_1:11;

then A8: |.(s . (n + 1)).| <= K by A4, A7;

A9: |.s.| ^2 = (|.sn.| ^2) + ((s . (n + 1)) ^2) by REAL_NS1:10;

A10: K >= 0 by A8, COMPLEX1:46;

A11: |.sn.| ^2 <= (n * K) ^2 by A3, A5, SQUARE_1:15;

A12: (s . (n + 1)) ^2 <= K ^2 by A8, SERIES_3:24;

A13: (((n * K) ^2) + (K ^2)) + ((2 * (n * K)) * K) >= ((n * K) ^2) + (K ^2) by A10, XREAL_1:38;

(|.sn.| ^2) + ((s . (n + 1)) ^2) <= ((n * K) ^2) + (K ^2) by A11, A12, XREAL_1:7;

then A14: |.s.| ^2 <= ((n + 1) * K) ^2 by A9, A13, XXREAL_0:2;

A15: sqrt (((n + 1) * K) ^2) = |.((n + 1) * K).| by COMPLEX1:72;

sqrt (|.s.| ^2) <= sqrt (((n + 1) * K) ^2) by A14, SQUARE_1:26;

then |.|.|.s.|.|.| <= sqrt (((n + 1) * K) ^2) by COMPLEX1:72;

then |.s.| <= sqrt (((n + 1) * K) ^2) by ABSVALUE:def 1;

hence |.s.| <= (n + 1) * K by A10, A15, ABSVALUE:def 1; :: thesis: verum

end;assume A3: S

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

|.(s . i).| <= K ) implies |.s.| <= (n + 1) * K )

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

|.(s . i).| <= K ; :: thesis: |.s.| <= (n + 1) * K

set sn = s | n;

len s = n + 1 by CARD_1:def 7;

then len (s | n) = n by FINSEQ_3:53;

then reconsider sn = s | n as Element of REAL n by FINSEQ_2:92;

A5: now :: thesis: for i being Element of NAT st 1 <= i & i <= n holds

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

A7:
n + 1 in NAT
by ORDINAL1:def 12;|.(sn . i).| <= K

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= n implies |.(sn . i).| <= K )

assume A6: ( 1 <= i & i <= n ) ; :: thesis: |.(sn . i).| <= K

n <= n + 1 by NAT_1:11;

then ( 1 <= i & i <= n + 1 ) by A6, XXREAL_0:2;

then |.(s . i).| <= K by A4;

hence |.(sn . i).| <= K by A6, FINSEQ_3:112; :: thesis: verum

end;assume A6: ( 1 <= i & i <= n ) ; :: thesis: |.(sn . i).| <= K

n <= n + 1 by NAT_1:11;

then ( 1 <= i & i <= n + 1 ) by A6, XXREAL_0:2;

then |.(s . i).| <= K by A4;

hence |.(sn . i).| <= K by A6, FINSEQ_3:112; :: thesis: verum

( 1 <= n + 1 & n + 1 <= n + 1 ) by NAT_1:11;

then A8: |.(s . (n + 1)).| <= K by A4, A7;

A9: |.s.| ^2 = (|.sn.| ^2) + ((s . (n + 1)) ^2) by REAL_NS1:10;

A10: K >= 0 by A8, COMPLEX1:46;

A11: |.sn.| ^2 <= (n * K) ^2 by A3, A5, SQUARE_1:15;

A12: (s . (n + 1)) ^2 <= K ^2 by A8, SERIES_3:24;

A13: (((n * K) ^2) + (K ^2)) + ((2 * (n * K)) * K) >= ((n * K) ^2) + (K ^2) by A10, XREAL_1:38;

(|.sn.| ^2) + ((s . (n + 1)) ^2) <= ((n * K) ^2) + (K ^2) by A11, A12, XREAL_1:7;

then A14: |.s.| ^2 <= ((n + 1) * K) ^2 by A9, A13, XXREAL_0:2;

A15: sqrt (((n + 1) * K) ^2) = |.((n + 1) * K).| by COMPLEX1:72;

sqrt (|.s.| ^2) <= sqrt (((n + 1) * K) ^2) by A14, SQUARE_1:26;

then |.|.|.s.|.|.| <= sqrt (((n + 1) * K) ^2) by COMPLEX1:72;

then |.s.| <= sqrt (((n + 1) * K) ^2) by ABSVALUE:def 1;

hence |.s.| <= (n + 1) * K by A10, A15, ABSVALUE:def 1; :: thesis: verum