set P = Partial_Sums f;
let m be Nat; :: according to SEQM_3:def 3 :: thesis: for b₁ being set holds
( not m in dom (Partial_Sums f) or not b₁ in dom (Partial_Sums f) or not m <= b₁ or (Partial_Sums f) . m <= (Partial_Sums f) . b₁ )
let n be Nat; :: thesis: ( not m in dom (Partial_Sums f) or not n in dom (Partial_Sums f) or not m <= n or (Partial_Sums f) . m <= (Partial_Sums f) . n )
assume ( m in dom (Partial_Sums f) & n in dom (Partial_Sums f) ) ; :: thesis: ( not m <= n or (Partial_Sums f) . m <= (Partial_Sums f) . n )
defpred S₁[ Nat] means ( m <= f implies (Partial_Sums f) . m <= (Partial_Sums f) . f );
A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
assume m <= k + 1 ; :: thesis: (Partial_Sums f) . m <= (Partial_Sums f) . (k + 1)

per cases then ( m <= k or m = k + 1 ) by NAT_1:8;

suppose A4: m <= k ; :: thesis: (Partial_Sums f) . m <= (Partial_Sums f) . (k + 1)

A5: (Partial_Sums f) . (k + 1) = ((Partial_Sums f) . k) + (f . (k + 1)) by SERIES_1:def 1;
dom f = NAT by PARTFUN1:def 2;
then f . (k + 1) in rng f by FUNCT_1:def 3;
then ((Partial_Sums f) . k) + 0 <= ((Partial_Sums f) . k) + (f . (k + 1)) by XREAL_1:6, PARTFUN3:def 4;
hence (Partial_Sums f) . m <= (Partial_Sums f) . (k + 1) by A3, A4, A5, XXREAL_0:2; :: thesis: verum

end;

suppose m = k + 1 ; :: thesis: (Partial_Sums f) . m <= (Partial_Sums f) . (k + 1)

hence (Partial_Sums f) . m <= (Partial_Sums f) . (k + 1) ; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence ( not m <= n or (Partial_Sums f) . m <= (Partial_Sums f) . n ) ; :: thesis: verum