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

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

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

then
Sum (sqr F0) <= Sum (sqr G)
by RVSUM_1:82;
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;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

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