let s1, s2 be Real_Sequence; :: thesis: ( ( for n being Nat holds s1 . n <= s2 . n ) implies for n being Nat holds (Partial_Sums s1) . n <= (Partial_Sums s2) . n )

defpred S_{1}[ Nat] means (Partial_Sums s1) . $1 <= (Partial_Sums s2) . $1;

assume A1: for n being Nat holds s1 . n <= s2 . n ; :: thesis: for n being Nat holds (Partial_Sums s1) . n <= (Partial_Sums s2) . n

A2: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

then A5: S_{1}[ 0 ]
by A1;

thus for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A5, A2); :: thesis: verum

defpred S

assume A1: for n being Nat holds s1 . n <= s2 . n ; :: thesis: for n being Nat holds (Partial_Sums s1) . n <= (Partial_Sums s2) . n

A2: for n being Nat st S

S

proof

( (Partial_Sums s2) . 0 = s2 . 0 & (Partial_Sums s1) . 0 = s1 . 0 )
by Def1;
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A3: (Partial_Sums s1) . n <= (Partial_Sums s2) . n ; :: thesis: S_{1}[n + 1]

A4: s1 . (n + 1) <= s2 . (n + 1) by A1;

( (Partial_Sums s1) . (n + 1) = ((Partial_Sums s1) . n) + (s1 . (n + 1)) & (Partial_Sums s2) . (n + 1) = ((Partial_Sums s2) . n) + (s2 . (n + 1)) ) by Def1;

hence S_{1}[n + 1]
by A3, A4, XREAL_1:7; :: thesis: verum

end;assume A3: (Partial_Sums s1) . n <= (Partial_Sums s2) . n ; :: thesis: S

A4: s1 . (n + 1) <= s2 . (n + 1) by A1;

( (Partial_Sums s1) . (n + 1) = ((Partial_Sums s1) . n) + (s1 . (n + 1)) & (Partial_Sums s2) . (n + 1) = ((Partial_Sums s2) . n) + (s2 . (n + 1)) ) by Def1;

hence S

then A5: S

thus for n being Nat holds S