let K be Real; :: thesis: for n being Element of NAT
for s being Element of REAL n st ( for i being Element of NAT st 1 <= i & i <= n holds
abs (s . i) <= K ) holds
|.s.| <= n * K
defpred S₁[ Nat] means for s being Element of REAL $1 st ( for i being Element of NAT st 1 <= i & i <= $1 holds
abs (s . i) <= K ) holds
|.s.| <= $1 * K;
A1: S₁[ 0 ]

proof

let s be Element of REAL 0; :: thesis: ( ( for i being Element of NAT st 1 <= i & i <= 0 holds
abs (s . i) <= K ) implies |.s.| <= 0 * K )
s = 0* 0 ;
hence ( ( for i being Element of NAT st 1 <= i & i <= 0 holds
abs (s . i) <= K ) implies |.s.| <= 0 * K ) by EUCLID:7; :: thesis: verum

end;

A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
let s be Element of REAL (n + 1); :: thesis: ( ( for i being Element of NAT st 1 <= i & i <= n + 1 holds
abs (s . i) <= K ) implies |.s.| <= (n + 1) * K )
assume A4: for i being Element of NAT st 1 <= i & i <= n + 1 holds
abs (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

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= n implies abs (sn . i) <= K )
assume A6: ( 1 <= i & i <= n ) ; :: thesis: abs (sn . i) <= K
n <= n + 1 by NAT_1:11;
then ( 1 <= i & i <= n + 1 ) by A6, XXREAL_0:2;
then abs (s . i) <= K by A4;
hence abs (sn . i) <= K by A6, FINSEQ_3:112; :: thesis: verum

end;

( 1 <= n + 1 & n + 1 <= n + 1 ) by NAT_1:11;
then A7: abs (s . (n + 1)) <= K by A4;
A8: |.s.| ^2 = (|.sn.| ^2) + ((s . (n + 1)) ^2) by REAL_NS1:10;
A9: K >= 0 by A7, COMPLEX1:46;
A10: |.sn.| ^2 <= (n * K) ^2 by A3, A5, SQUARE_1:15;
A11: (s . (n + 1)) ^2 <= K ^2 by A7, SERIES_3:24;
A12: (((n * K) ^2) + (K ^2)) + ((2 * (n * K)) * K) >= ((n * K) ^2) + (K ^2) by A9, XREAL_1:38;
(|.sn.| ^2) + ((s . (n + 1)) ^2) <= ((n * K) ^2) + (K ^2) by A10, A11, XREAL_1:7;
then A13: |.s.| ^2 <= ((n + 1) * K) ^2 by A8, A12, XXREAL_0:2;
A14: sqrt (((n + 1) * K) ^2) = |.((n + 1) * K).| by COMPLEX1:72;
sqrt (|.s.| ^2) <= sqrt (((n + 1) * K) ^2) by A13, SQUARE_1:26;
then abs (abs |.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 A9, A14, ABSVALUE:def 1; :: thesis: verum

end;

thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2); :: thesis: verum