let f1, f2 be Real_Sequence; :: thesis: for n being non trivial Nat st ( for k being non trivial Nat st k <= n holds
f1 . k < f2 . k ) holds
Sum (f1,n,1) < Sum (f2,n,1)
let n be non trivial Nat; :: thesis: ( ( for k being non trivial Nat st k <= n holds
f1 . k < f2 . k ) implies Sum (f1,n,1) < Sum (f2,n,1) )
assume A1: for k being non trivial Nat st k <= n holds
f1 . k < f2 . k ; :: thesis: Sum (f1,n,1) < Sum (f2,n,1)
defpred S₁[ Nat] means ( ( for k being non trivial Nat st k <= $1 holds
f1 . k < f2 . k ) implies ((Partial_Sums f1) . $1) - ((Partial_Sums f1) . 1) < ((Partial_Sums f2) . $1) - ((Partial_Sums f2) . 1) );
( (Partial_Sums f1) . 2 = ((Partial_Sums f1) . 1) + (f1 . (1 + 1)) & (Partial_Sums f2) . 2 = ((Partial_Sums f2) . 1) + (f2 . (1 + 1)) ) by SERIES_1:def 1;
then a1: S₁[2] ;
A2: for n being non trivial Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non trivial Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
assume B1: for k being non trivial Nat st k <= n + 1 holds
f1 . k < f2 . k ; :: thesis: ((Partial_Sums f1) . (n + 1)) - ((Partial_Sums f1) . 1) < ((Partial_Sums f2) . (n + 1)) - ((Partial_Sums f2) . 1)
A4: f1 . (n + 1) < f2 . (n + 1) by B1;
ZZ: ( (Partial_Sums f1) . (n + 1) = ((Partial_Sums f1) . n) + (f1 . (n + 1)) & (Partial_Sums f2) . (n + 1) = ((Partial_Sums f2) . n) + (f2 . (n + 1)) ) by SERIES_1:def 1;
G1: n <= n + 1 by NAT_1:11;
for k being non trivial Nat st k <= n holds
f1 . k < f2 . k

proof

let k be non trivial Nat; :: thesis: ( k <= n implies f1 . k < f2 . k )
assume k <= n ; :: thesis: f1 . k < f2 . k
then k <= n + 1 by G1, XXREAL_0:2;
hence f1 . k < f2 . k by B1; :: thesis: verum

end;

then (f1 . (n + 1)) + (((Partial_Sums f1) . n) - ((Partial_Sums f1) . 1)) < (f2 . (n + 1)) + (((Partial_Sums f2) . n) - ((Partial_Sums f2) . 1)) by A3, A4, XREAL_1:8;
hence ((Partial_Sums f1) . (n + 1)) - ((Partial_Sums f1) . 1) < ((Partial_Sums f2) . (n + 1)) - ((Partial_Sums f2) . 1) by ZZ; :: thesis: verum

end;

for n being non trivial Nat holds S₁[n] from NAT_2:sch 2(a1, A2);
hence Sum (f1,n,1) < Sum (f2,n,1) by A1; :: thesis: verum