theorem :: SERIES_3:52

for s1, s2, s3, s4, s5 being Real_Sequence st s4 = s1 (#) s1 & s5 = s2 (#) s2 & ( for n being Nat holds
( s1 . n >= 0 & s2 . n >= 0 & s3 . n = ((s1 . n) + (s2 . n)) ^2 ) ) holds
for n being Nat holds sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n))