let s1, s2, s3, s4, s5 be Real_Sequence; :: thesis: ( s4 = s1 (#) s1 & s5 = s2 (#) s2 & ( for n being Nat holds
( s1 . n >= 0 & s2 . n >= 0 & s3 . n = ((s1 . n) + (s2 . n)) ^2 ) ) implies for n being Nat holds sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n)) )
assume that
A1: s4 = s1 (#) s1 and
A2: s5 = s2 (#) s2 and
A3: for n being Nat holds
( s1 . n >= 0 & s2 . n >= 0 & s3 . n = ((s1 . n) + (s2 . n)) ^2 ) ; :: thesis: for n being Nat holds sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n))
A4: s1 . 0 >= 0 by A3;
defpred S₁[ Nat] means sqrt ((Partial_Sums s3) . $1) <= (sqrt ((Partial_Sums s4) . $1)) + (sqrt ((Partial_Sums s5) . $1));
A5: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n)) ; :: thesis: S₁[n + 1]
set j = s2 . (n + 1);
set h = s1 . (n + 1);
set w = (Partial_Sums s5) . n;
set v = (Partial_Sums s4) . n;
set u = (Partial_Sums s3) . n;
A7: (Partial_Sums s5) . n >= 0 by A2, Th36;
A8: (s2 . (n + 1)) ^2 >= 0 by XREAL_1:63;
then A9: sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)) >= 0 by A7, SQUARE_1:def 2;
A10: (Partial_Sums s4) . n >= 0 by A1, Th36;
then A11: sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) >= 0 by A7, SQUARE_1:def 2;
A12: (Partial_Sums s3) . n >= 0 by A3, Lm10;
then sqrt ((Partial_Sums s3) . n) >= 0 by SQUARE_1:def 2;
then (sqrt ((Partial_Sums s3) . n)) ^2 <= ((sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n))) ^2 by A6, SQUARE_1:15;
then (Partial_Sums s3) . n <= (((sqrt ((Partial_Sums s4) . n)) ^2) + ((2 * (sqrt ((Partial_Sums s4) . n))) * (sqrt ((Partial_Sums s5) . n)))) + ((sqrt ((Partial_Sums s5) . n)) ^2) by A12, SQUARE_1:def 2;
then (Partial_Sums s3) . n <= (((Partial_Sums s4) . n) + ((2 * (sqrt ((Partial_Sums s4) . n))) * (sqrt ((Partial_Sums s5) . n)))) + ((sqrt ((Partial_Sums s5) . n)) ^2) by A10, SQUARE_1:def 2;
then (Partial_Sums s3) . n <= (((Partial_Sums s4) . n) + ((2 * (sqrt ((Partial_Sums s4) . n))) * (sqrt ((Partial_Sums s5) . n)))) + ((Partial_Sums s5) . n) by A7, SQUARE_1:def 2;
then ((Partial_Sums s3) . n) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1))) <= ((((Partial_Sums s4) . n) + ((Partial_Sums s5) . n)) + (2 * ((sqrt ((Partial_Sums s4) . n)) * (sqrt ((Partial_Sums s5) . n))))) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1))) by XREAL_1:6;
then A13: ((Partial_Sums s3) . n) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1))) <= ((((Partial_Sums s4) . n) + ((Partial_Sums s5) . n)) + (2 * (sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))))) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1))) by A10, A7, SQUARE_1:29;
A14: s1 . (n + 1) >= 0 by A3;
A15: s2 . (n + 1) >= 0 by A3;
A16: (s1 . (n + 1)) ^2 >= 0 by XREAL_1:63;
then A17: sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) >= 0 by A10, SQUARE_1:def 2;
(((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= 2 * (sqrt ((((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) * (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)))) by A10, A7, A16, A8, SIN_COS2:1;
then (((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= 2 * (sqrt ((((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n)))) ;
then (((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= 2 * ((sqrt (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n)))) by A10, A7, A16, A8, SQUARE_1:29;
then (((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= (2 * (sqrt (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2)))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n))) ;
then (((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= (2 * ((sqrt ((s1 . (n + 1)) ^2)) * (sqrt ((s2 . (n + 1)) ^2)))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n))) by A16, A8, SQUARE_1:29;
then (((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= ((2 * (sqrt ((s1 . (n + 1)) ^2))) * (sqrt ((s2 . (n + 1)) ^2))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n))) ;
then (((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= ((2 * (s1 . (n + 1))) * (sqrt ((s2 . (n + 1)) ^2))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n))) by A14, SQUARE_1:22;
then (((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= ((2 * (s1 . (n + 1))) * (s2 . (n + 1))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n))) by A15, SQUARE_1:22;
then ((((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n))) + ((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) + (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2))) >= (((2 * (s1 . (n + 1))) * (s2 . (n + 1))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n)))) + ((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) + (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2))) by XREAL_1:6;
then (((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n))) + (((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n))) + (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2)) >= ((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) + ((2 * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n)))) * ((s1 . (n + 1)) * (s2 . (n + 1))))) + (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2)) ;
then ( ((sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))) + ((s1 . (n + 1)) * (s2 . (n + 1)))) ^2 >= 0 & (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)) >= (((sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))) ^2) + ((2 * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n)))) * ((s1 . (n + 1)) * (s2 . (n + 1))))) + (((s1 . (n + 1)) * (s2 . (n + 1))) ^2) ) by A10, A7, SQUARE_1:def 2, XREAL_1:63;
then sqrt (((sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))) + ((s1 . (n + 1)) * (s2 . (n + 1)))) ^2) <= sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2))) by SQUARE_1:26;
then (sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))) + ((s1 . (n + 1)) * (s2 . (n + 1))) <= sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2))) by A14, A15, A11, SQUARE_1:22;
then 2 * ((sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))) + ((s1 . (n + 1)) * (s2 . (n + 1)))) <= 2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))) by XREAL_1:64;
then (((Partial_Sums s4) . n) + ((Partial_Sums s5) . n)) + ((2 * (sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)))) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1)))) <= (((Partial_Sums s4) . n) + ((Partial_Sums s5) . n)) + (2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2))))) by XREAL_1:6;
then ((Partial_Sums s3) . n) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1))) <= (((Partial_Sums s4) . n) + ((Partial_Sums s5) . n)) + (2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2))))) by A13, XXREAL_0:2;
then (((Partial_Sums s3) . n) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1)))) + (((s1 . (n + 1)) ^2) + ((s2 . (n + 1)) ^2)) <= ((((Partial_Sums s4) . n) + ((Partial_Sums s5) . n)) + (2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))))) + (((s1 . (n + 1)) ^2) + ((s2 . (n + 1)) ^2)) by XREAL_1:6;
then ((Partial_Sums s3) . n) + ((((s1 . (n + 1)) ^2) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1)))) + ((s2 . (n + 1)) ^2)) <= ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) + (2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))))) + (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)) ;
then ((Partial_Sums s3) . n) + (((s1 . (n + 1)) + (s2 . (n + 1))) ^2) <= (((sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2))) ^2) + (2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))))) + (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)) by A10, A16, SQUARE_1:def 2;
then ((Partial_Sums s3) . n) + (((s1 . (n + 1)) + (s2 . (n + 1))) ^2) <= (((sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2))) ^2) + (2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))))) + ((sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2))) ^2) by A7, A8, SQUARE_1:def 2;
then ( ((s1 . (n + 1)) + (s2 . (n + 1))) ^2 >= 0 & ((Partial_Sums s3) . n) + (((s1 . (n + 1)) + (s2 . (n + 1))) ^2) <= (((sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2))) ^2) + (2 * ((sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2))) * (sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))))) + ((sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2))) ^2) ) by A10, A7, A16, A8, SQUARE_1:29, XREAL_1:63;
then A18: sqrt (((Partial_Sums s3) . n) + (((s1 . (n + 1)) + (s2 . (n + 1))) ^2)) <= sqrt (((sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2))) + (sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))) ^2) by A12, SQUARE_1:26;
A19: sqrt ((Partial_Sums s3) . (n + 1)) = sqrt (((Partial_Sums s3) . n) + (s3 . (n + 1))) by SERIES_1:def 1
.= sqrt (((Partial_Sums s3) . n) + (((s1 . (n + 1)) + (s2 . (n + 1))) ^2)) by A3 ;
(sqrt ((Partial_Sums s4) . (n + 1))) + (sqrt ((Partial_Sums s5) . (n + 1))) = (sqrt (((Partial_Sums s4) . n) + (s4 . (n + 1)))) + (sqrt ((Partial_Sums s5) . (n + 1))) by SERIES_1:def 1
.= (sqrt (((Partial_Sums s4) . n) + (s4 . (n + 1)))) + (sqrt (((Partial_Sums s5) . n) + (s5 . (n + 1)))) by SERIES_1:def 1
.= (sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) * (s1 . (n + 1))))) + (sqrt (((Partial_Sums s5) . n) + (s5 . (n + 1)))) by A1, SEQ_1:8
.= (sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2))) + (sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2))) by A2, SEQ_1:8 ;
hence S₁[n + 1] by A19, A17, A9, A18, SQUARE_1:22; :: thesis: verum

end;

A20: s2 . 0 >= 0 by A3;
(sqrt ((Partial_Sums s4) . 0)) + (sqrt ((Partial_Sums s5) . 0)) = (sqrt (s4 . 0)) + (sqrt ((Partial_Sums s5) . 0)) by SERIES_1:def 1
.= (sqrt (s4 . 0)) + (sqrt (s5 . 0)) by SERIES_1:def 1
.= (sqrt ((s1 . 0) * (s1 . 0))) + (sqrt (s5 . 0)) by A1, SEQ_1:8
.= (sqrt ((s1 . 0) ^2)) + (sqrt ((s2 . 0) * (s2 . 0))) by A2, SEQ_1:8
.= (s1 . 0) + (sqrt ((s2 . 0) ^2)) by A4, SQUARE_1:22
.= (s1 . 0) + (s2 . 0) by A20, SQUARE_1:22
.= sqrt (((s1 . 0) + (s2 . 0)) ^2) by A4, A20, SQUARE_1:22
.= sqrt (s3 . 0) by A3
.= sqrt ((Partial_Sums s3) . 0) by SERIES_1:def 1 ;
then A21: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A21, A5);
hence for n being Nat holds sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n)) ; :: thesis: verum