let s1, s2 be Real_Sequence; :: thesis: (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2)
A1: now :: thesis: for n being Nat holds ((Partial_Sums s1) - (Partial_Sums s2)) . (n + 1) = (((Partial_Sums s1) - (Partial_Sums s2)) . n) + ((s1 - s2) . (n + 1))
let n be Nat; :: thesis: ((Partial_Sums s1) - (Partial_Sums s2)) . (n + 1) = (((Partial_Sums s1) - (Partial_Sums s2)) . n) + ((s1 - s2) . (n + 1))
thus ((Partial_Sums s1) - (Partial_Sums s2)) . (n + 1) = ((Partial_Sums s1) . (n + 1)) - ((Partial_Sums s2) . (n + 1)) by RFUNCT_2:1
.= (((Partial_Sums s1) . n) + (s1 . (n + 1))) - ((Partial_Sums s2) . (n + 1)) by Def1
.= (((Partial_Sums s1) . n) + (s1 . (n + 1))) - ((s2 . (n + 1)) + ((Partial_Sums s2) . n)) by Def1
.= (((Partial_Sums s1) . n) + ((s1 . (n + 1)) - (s2 . (n + 1)))) - ((Partial_Sums s2) . n)
.= (((s1 - s2) . (n + 1)) + ((Partial_Sums s1) . n)) - ((Partial_Sums s2) . n) by RFUNCT_2:1
.= ((s1 - s2) . (n + 1)) + (((Partial_Sums s1) . n) - ((Partial_Sums s2) . n))
.= (((Partial_Sums s1) - (Partial_Sums s2)) . n) + ((s1 - s2) . (n + 1)) by RFUNCT_2:1 ; :: thesis: verum
end;
((Partial_Sums s1) - (Partial_Sums s2)) . 0 = ((Partial_Sums s1) . 0) - ((Partial_Sums s2) . 0) by RFUNCT_2:1
.= (s1 . 0) - ((Partial_Sums s2) . 0) by Def1
.= (s1 . 0) - (s2 . 0) by Def1
.= (s1 - s2) . 0 by RFUNCT_2:1 ;
hence (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2) by A1, Def1; :: thesis: verum