let n be Nat; :: thesis: for F being Element of REAL n
for s being Real st ( for i being Nat st i in dom F holds
( 0 <= F . i & F . i <= s ) ) holds
|.F.| <= sqrt ((s * s) * (len F))

let F be Element of REAL n; :: thesis: for s being Real st ( for i being Nat st i in dom F holds
( 0 <= F . i & F . i <= s ) ) holds
|.F.| <= sqrt ((s * s) * (len F))

let s be Real; :: thesis: ( ( for i being Nat st i in dom F holds
( 0 <= F . i & F . i <= s ) ) implies |.F.| <= sqrt ((s * s) * (len F)) )

assume A1: for i being Nat st i in dom F holds
( 0 <= F . i & F . i <= s ) ; :: thesis: |.F.| <= sqrt ((s * s) * (len F))
A2: 0 <= Sum (sqr F) by RVSUM_1:86;
set G = (len F) |-> s;
A3: sqr ((len F) |-> s) = (len F) |-> (s ^2) by RVSUM_1:56;
( len F is natural Number & s is Element of REAL ) by XREAL_0:def 1;
then reconsider G = (len F) |-> s as Element of (len F) -tuples_on REAL by FINSEQ_2:112;
reconsider F0 = F as Element of (len F) -tuples_on REAL by FINSEQ_2:92;
for j being Nat st j in Seg (len F0) holds
(sqr F0) . j <= (sqr G) . j
proof
let j be Nat; :: thesis: ( j in Seg (len F0) implies (sqr F0) . j <= (sqr G) . j )
assume A4: j in Seg (len F0) ; :: thesis: (sqr F0) . j <= (sqr G) . j
then A5: j in dom F by FINSEQ_1:def 3;
A6: (sqr F0) . j = (F . j) ^2 by VALUED_1:11;
A7: (sqr G) . j = (G . j) ^2 by VALUED_1:11;
A8: 0 <= F0 . j by A1, A5;
F0 . j <= s by A1, A5;
then F0 . j <= G . j by ;
hence (sqr F0) . j <= (sqr G) . j by ; :: thesis: verum
end;
then Sum (sqr F0) <= Sum (sqr G) by RVSUM_1:82;
then Sum (sqr F) <= (s * s) * (len F) by ;
hence |.F.| <= sqrt ((s * s) * (len F)) by ; :: thesis: verum