let s1, s2 be Real_Sequence; :: thesis: ( ( for n being Nat holds
( s1 . n >= 0 & s2 . n >= 0 ) ) implies for n being Nat holds ((Partial_Product s1) . n) + ((Partial_Product s2) . n) <= (Partial_Product (s1 + s2)) . n )
set s = s1 + s2;
defpred S₁[ Nat] means ((Partial_Product s1) . $1) + ((Partial_Product s2) . $1) <= (Partial_Product (s1 + s2)) . $1;
A1: (Partial_Product (s1 + s2)) . 0 = (s1 + s2) . 0 by Def1
.= (s1 . 0) + (s2 . 0) by SEQ_1:7 ;
assume A2: for n being Nat holds
( s1 . n >= 0 & s2 . n >= 0 ) ; :: thesis: for n being Nat holds ((Partial_Product s1) . n) + ((Partial_Product s2) . n) <= (Partial_Product (s1 + s2)) . n
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set u = (Partial_Product s1) . n;
set v = (Partial_Product s2) . n;
set w = (Partial_Product (s1 + s2)) . n;
set h = s1 . (n + 1);
set j = s2 . (n + 1);
A4: ( s1 . (n + 1) >= 0 & s2 . (n + 1) >= 0 ) by A2;
( (Partial_Product s1) . n >= 0 & (Partial_Product s2) . n >= 0 ) by A2, Th44;
then A5: (((Partial_Product s1) . n) * (s1 . (n + 1))) + (((Partial_Product s2) . n) * (s2 . (n + 1))) <= ((((Partial_Product s1) . n) * (s1 . (n + 1))) + (((Partial_Product s2) . n) * (s2 . (n + 1)))) + ((((Partial_Product s1) . n) * (s2 . (n + 1))) + (((Partial_Product s2) . n) * (s1 . (n + 1)))) by A4, XREAL_1:31;
A6: (Partial_Product (s1 + s2)) . (n + 1) = ((Partial_Product (s1 + s2)) . n) * ((s1 + s2) . (n + 1)) by Def1
.= ((Partial_Product (s1 + s2)) . n) * ((s1 . (n + 1)) + (s2 . (n + 1))) by SEQ_1:7 ;
assume ((Partial_Product s1) . n) + ((Partial_Product s2) . n) <= (Partial_Product (s1 + s2)) . n ; :: thesis: S₁[n + 1]
then A7: (((Partial_Product s1) . n) + ((Partial_Product s2) . n)) * ((s1 . (n + 1)) + (s2 . (n + 1))) <= ((Partial_Product (s1 + s2)) . n) * ((s1 . (n + 1)) + (s2 . (n + 1))) by A4, XREAL_1:64;
((Partial_Product s1) . (n + 1)) + ((Partial_Product s2) . (n + 1)) = (((Partial_Product s1) . n) * (s1 . (n + 1))) + ((Partial_Product s2) . (n + 1)) by Def1
.= (((Partial_Product s1) . n) * (s1 . (n + 1))) + (((Partial_Product s2) . n) * (s2 . (n + 1))) by Def1 ;
hence S₁[n + 1] by A7, A6, A5, XXREAL_0:2; :: thesis: verum

end;

((Partial_Product s1) . 0) + ((Partial_Product s2) . 0) = (s1 . 0) + ((Partial_Product s2) . 0) by Def1
.= (s1 . 0) + (s2 . 0) by Def1 ;
then A8: S₁[ 0 ] by A1;
for n being Nat holds S₁[n] from NAT_1:sch 2(A8, A3);
hence for n being Nat holds ((Partial_Product s1) . n) + ((Partial_Product s2) . n) <= (Partial_Product (s1 + s2)) . n ; :: thesis: verum