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 A4, FINSEQ_2:57;
hence (sqr F0) . j <= (sqr G) . j by A6, A7, A8, SQUARE_1:15; :: thesis: verum
end;
then Sum (sqr F0) <= Sum (sqr G) by RVSUM_1:82;
then Sum (sqr F) <= (s * s) * (len F) by A3, RVSUM_1:80;
hence |.F.| <= sqrt ((s * s) * (len F)) by A2, SQUARE_1:26; :: thesis: verum