let s4, s1, s5, s2, s3 be Real_Sequence; :: thesis: ( s4 = s1 (#) s1 & s5 = s2 (#) s2 & ( for n being Element of NAT holds
( s1 . n >= 0 & s2 . n >= 0 & s3 . n = ((s1 . n) + (s2 . n)) ^2 ) ) implies for n being Element of 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 Element of NAT holds
( s1 . n >= 0 & s2 . n >= 0 & s3 . n = ((s1 . n) + (s2 . n)) ^2 ) ; :: thesis: for n being Element of 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₁[ Element of NAT ] means sqrt ((Partial_Sums s3) . $1) <= (sqrt ((Partial_Sums s4) . $1)) + (sqrt ((Partial_Sums s5) . $1));
A5: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of 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:65;
then A9: sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2 )) >= 0 by A7, SQUARE_1:def 4;
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 4;
A12: (Partial_Sums s3) . n >= 0 by A3, Lm11;
then sqrt ((Partial_Sums s3) . n) >= 0 by SQUARE_1:def 4;
then (sqrt ((Partial_Sums s3) . n)) ^2 <= ((sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n))) ^2 by A6, SQUARE_1:77;
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 4;
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 4;
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 4;
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:8;
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:97;
A14: s1 . (n + 1) >= 0 by A3;
A15: s2 . (n + 1) >= 0 by A3;
A16: (s1 . (n + 1)) ^2 >= 0 by XREAL_1:65;
then A17: sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2 )) >= 0 by A10, SQUARE_1:def 4;
(((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:97;
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:97;
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:89;
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:89;
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:8;
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 4, XREAL_1:65;
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:94;
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:89;
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:66;
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:8;
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:8;
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 4;
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 4;
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:97, XREAL_1:65;
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:94;
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:12
.= (sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2 ))) + (sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2 ))) by A2, SEQ_1:12 ;
hence S₁[n + 1] by A19, A17, A9, A18, SQUARE_1:89; :: 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:12
.= (sqrt ((s1 . 0 ) ^2 )) + (sqrt ((s2 . 0 ) * (s2 . 0 ))) by A2, SEQ_1:12
.= (s1 . 0 ) + (sqrt ((s2 . 0 ) ^2 )) by A4, SQUARE_1:89
.= (s1 . 0 ) + (s2 . 0 ) by A20, SQUARE_1:89
.= sqrt (((s1 . 0 ) + (s2 . 0 )) ^2 ) by A4, A20, SQUARE_1:89
.= sqrt (s3 . 0 ) by A3
.= sqrt ((Partial_Sums s3) . 0 ) by SERIES_1:def 1 ;
then A21: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A21, A5);
hence for n being Element of NAT holds sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n)) ; :: thesis: verum