let n be Nat; :: thesis: for X being RealUnitarySpace
for seq being sequence of X holds seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n))
let X be RealUnitarySpace; :: thesis: for seq being sequence of X holds seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n))
let seq be sequence of X; :: thesis: seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n))
thus (Sum (seq,(n + 1))) - (Sum (seq,n)) = ((seq . (n + 1)) + (Sum (seq,n))) - (Sum (seq,n)) by Def1
.= (seq . (n + 1)) + ((Sum (seq,n)) - (Sum (seq,n))) by RLVECT_1:def 3
.= (seq . (n + 1)) + (0. X) by RLVECT_1:15
.= seq . (n + 1) ; :: thesis: verum