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₁[ 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₁[ 0 ]

proof

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;

A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be 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
|.(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

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;

A7: n + 1 in NAT by ORDINAL1:def 12;
( 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;

thus for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2); :: thesis: verum