let rf be real-valued FinSequence; :: thesis:
defpred S₁[ Nat] means for f being real-valued FinSequence st len f = $1 & f is nonnegative-yielding holds
( sqrt (Sum f) <= Sum (sqrt f) & 0 <= Sum f );
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A2: S₁[n] ; :: thesis:
set n1 = n + 1;
let f be real-valued FinSequence; :: thesis:
assume that
A3: len f = n + 1 and
A4: f is nonnegative-yielding ; :: thesis:
rng f c= REAL ;
then reconsider F = f as FinSequence of REAL by FINSEQ_1:def 4;
reconsider fn = F | n as FinSequence of REAL ;
A5: F = fn ^ <*(F . (n + 1))*> by A3, FINSEQ_3:55;
then sqrt F = (sqrt fn) ^ (sqrt <*(F . (n + 1))*>) by Th2
.= (sqrt fn) ^ <*(sqrt (F . (n + 1)))*> by Th3 ;
then A6: Sum (sqrt F) = (Sum (sqrt fn)) + (sqrt (F . (n + 1))) by RVSUM_1:74;
A7: len fn = n by A3, FINSEQ_3:53;
then sqrt (Sum fn) <= Sum (sqrt fn) by A2, A4;
then A8: (sqrt (Sum fn)) + (sqrt (f . (n + 1))) <= Sum (sqrt F) by A6, XREAL_1:6;
A9: Sum f = (Sum fn) + (f . (n + 1)) by A5, RVSUM_1:74;
n + 1 >= 1 by NAT_1:11;
then n + 1 in dom f by A3, FINSEQ_3:25;
then f . (n + 1) in rng f by FUNCT_1:def 3;
then A10: f . (n + 1) >= 0 by A4;
A11: Sum fn >= 0 by A2, A4, A7;
then sqrt (Sum f) <= (sqrt (Sum fn)) + (sqrt (f . (n + 1))) by A9, A10, SQUARE_1:59;
hence ( sqrt (Sum f) <= Sum (sqrt f) & 0 <= Sum f ) by A9, A11, A10, A8, XXREAL_0:2; :: thesis:

end;

A12: S₁[ 0 ]

proof

let f be real-valued FinSequence; :: thesis:
assume that
A13: len f = 0 and
f is nonnegative-yielding ; :: thesis:
dom f = dom (sqrt f) by PARTFUN3:def 5;
then len f = len (sqrt f) by FINSEQ_3:29;
then A14: sqrt f = <*> REAL by A13;
f = <*> REAL by A13;
hence ( sqrt (Sum f) <= Sum (sqrt f) & 0 <= Sum f ) by A14, RVSUM_1:72, SQUARE_1:17; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A12, A1);
then S₁[ len rf] ;
hence ( rf is nonnegative-yielding implies sqrt (Sum rf) <= Sum (sqrt rf) ) ; :: thesis: