let X be RealNormSpace; :: thesis: for s1, s2 being sequence of X holds (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2)
let s1, s2 be sequence of X; :: thesis: (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2)
A1: ((Partial_Sums s1) - (Partial_Sums s2)) . 0 = ((Partial_Sums s1) . 0 ) - ((Partial_Sums s2) . 0 ) by NORMSP_1:def 6
.= (s1 . 0 ) - ((Partial_Sums s2) . 0 ) by BHSP_4:def 1
.= (s1 . 0 ) - (s2 . 0 ) by BHSP_4:def 1
.= (s1 - s2) . 0 by NORMSP_1:def 6 ;

now

let n be Element of 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 NORMSP_1:def 6
.= (((Partial_Sums s1) . n) + (s1 . (n + 1))) - ((Partial_Sums s2) . (n + 1)) by BHSP_4:def 1
.= (((Partial_Sums s1) . n) + (s1 . (n + 1))) - ((s2 . (n + 1)) + ((Partial_Sums s2) . n)) by BHSP_4:def 1
.= ((((Partial_Sums s1) . n) + (s1 . (n + 1))) - (s2 . (n + 1))) - ((Partial_Sums s2) . n) by RLVECT_1:41
.= (((Partial_Sums s1) . n) + ((s1 . (n + 1)) - (s2 . (n + 1)))) - ((Partial_Sums s2) . n) by RLVECT_1:def 6
.= (((s1 - s2) . (n + 1)) + ((Partial_Sums s1) . n)) - ((Partial_Sums s2) . n) by NORMSP_1:def 6
.= ((s1 - s2) . (n + 1)) + (((Partial_Sums s1) . n) - ((Partial_Sums s2) . n)) by RLVECT_1:def 6
.= (((Partial_Sums s1) - (Partial_Sums s2)) . n) + ((s1 - s2) . (n + 1)) by NORMSP_1:def 6 ; :: thesis: verum

end;

hence (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2) by A1, BHSP_4:def 1; :: thesis: verum