let X be RealNormSpace; :: thesis: for s1, s2 being sequence of X holds () - () = Partial_Sums (s1 - s2)
let s1, s2 be sequence of X; :: thesis: () - () = Partial_Sums (s1 - s2)
A1: now :: thesis: for n being Nat holds (() - ()) . (n + 1) = ((() - ()) . n) + ((s1 - s2) . (n + 1))
let n be Nat; :: thesis: (() - ()) . (n + 1) = ((() - ()) . n) + ((s1 - s2) . (n + 1))
thus (() - ()) . (n + 1) = (() . (n + 1)) - (() . (n + 1)) by NORMSP_1:def 3
.= ((() . n) + (s1 . (n + 1))) - (() . (n + 1)) by BHSP_4:def 1
.= ((() . n) + (s1 . (n + 1))) - ((s2 . (n + 1)) + (() . n)) by BHSP_4:def 1
.= (((() . n) + (s1 . (n + 1))) - (s2 . (n + 1))) - (() . n) by RLVECT_1:27
.= ((() . n) + ((s1 . (n + 1)) - (s2 . (n + 1)))) - (() . n) by RLVECT_1:def 3
.= (((s1 - s2) . (n + 1)) + (() . n)) - (() . n) by NORMSP_1:def 3
.= ((s1 - s2) . (n + 1)) + ((() . n) - (() . n)) by RLVECT_1:def 3
.= ((() - ()) . n) + ((s1 - s2) . (n + 1)) by NORMSP_1:def 3 ; :: thesis: verum
end;
(() - ()) . 0 = (() . 0) - (() . 0) by NORMSP_1:def 3
.= (s1 . 0) - (() . 0) by BHSP_4:def 1
.= (s1 . 0) - (s2 . 0) by BHSP_4:def 1
.= (s1 - s2) . 0 by NORMSP_1:def 3 ;
hence (Partial_Sums s1) - () = Partial_Sums (s1 - s2) by ; :: thesis: verum