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 A1: ( 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 ) ) ) ; :: thesis: for n being Element of NAT holds sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n))
defpred S₁[ Element of NAT ] means sqrt ((Partial_Sums s3) . $1) <= (sqrt ((Partial_Sums s4) . $1)) + (sqrt ((Partial_Sums s5) . $1));
A2: ( s1 . 0 >= 0 & s2 . 0 >= 0 ) by A1;
(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 A1, SEQ_1:12
.= (s1 . 0 ) + (sqrt ((s2 . 0 ) ^2 )) by A2, SQUARE_1:89
.= (s1 . 0 ) + (s2 . 0 ) by A2, SQUARE_1:89
.= sqrt (((s1 . 0 ) + (s2 . 0 )) ^2 ) by A2, SQUARE_1:89
.= sqrt (s3 . 0 ) by A1
.= sqrt ((Partial_Sums s3) . 0 ) by SERIES_1:def 1 ;
then A3: S₁[ 0 ] ;
A4: 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 A5: sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n)) ; :: thesis: S₁[n + 1]
set u = (Partial_Sums s3) . n;
set v = (Partial_Sums s4) . n;
set w = (Partial_Sums s5) . n;
set h = s1 . (n + 1);
set j = s2 . (n + 1);
A6: (Partial_Sums s3) . n >= 0 by A1, Lm11;
then A7: sqrt ((Partial_Sums s3) . n) >= 0 by SQUARE_1:def 4;
A8: (Partial_Sums s4) . n >= 0 by A1, Th36;
A9: (Partial_Sums s5) . n >= 0 by A1, Th36;
(sqrt ((Partial_Sums s3) . n)) ^2 <= ((sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n))) ^2 by A5, A7, 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 A6, 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 A8, SQUARE_1:def 4;
then A10: (Partial_Sums s3) . n <= (((Partial_Sums s4) . n) + ((2 * (sqrt ((Partial_Sums s4) . n))) * (sqrt ((Partial_Sums s5) . n)))) + ((Partial_Sums s5) . n) by A9, SQUARE_1:def 4;
A11: 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 A1 ;
A12: (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 A1, SEQ_1:12 ;
A13: ( s1 . (n + 1) >= 0 & s2 . (n + 1) >= 0 ) by A1;
A14: ( (s1 . (n + 1)) ^2 >= 0 & (s2 . (n + 1)) ^2 >= 0 ) by XREAL_1:65;
then A15: ((s1 . (n + 1)) ^2 ) * ((s2 . (n + 1)) ^2 ) >= 0 ;
A16: ((Partial_Sums s5) . n) * ((Partial_Sums s4) . n) >= 0 by A8, A9;
A17: ((sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))) + ((s1 . (n + 1)) * (s2 . (n + 1)))) ^2 >= 0 by XREAL_1:65;
A18: sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) >= 0 by A16, SQUARE_1:def 4;
A19: (s1 . (n + 1)) * (s2 . (n + 1)) >= 0 by A13;
A20: ((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2 ) >= 0 by A8, A14;
A21: ((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2 ) >= 0 by A9, A14;
((s1 . (n + 1)) + (s2 . (n + 1))) ^2 >= 0 by XREAL_1:65;
then A22: ((Partial_Sums s3) . n) + (((s1 . (n + 1)) + (s2 . (n + 1))) ^2 ) >= 0 by A6;
A23: ( sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2 )) >= 0 & sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2 )) >= 0 ) by A20, A21, SQUARE_1:def 4;
( ((s1 . (n + 1)) ^2 ) * ((Partial_Sums s5) . n) >= 0 & ((s2 . (n + 1)) ^2 ) * ((Partial_Sums s4) . n) >= 0 ) by A8, A9, A14;
then (((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 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 A15, A16, 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 A14, 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 A13, 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 A13, 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 (((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 A16, SQUARE_1:def 4;
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 A17, 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 A18, A19, 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 A24: (((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;
((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 A10, 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) * ((Partial_Sums s5) . n))))) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1))) by A8, A9, SQUARE_1:97;
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 A24, 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 A20, 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 A21, 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 ))) * (sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2 )))))) + ((sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2 ))) ^2 ) by A20, A21, SQUARE_1:97;
then 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 A22, SQUARE_1:94;
hence S₁[n + 1] by A11, A12, A23, SQUARE_1:89; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A4);
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