let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for n being Nat holds seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n))
let seq be sequence of X; :: thesis: for n being Nat holds seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n))
let n be Nat; :: 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 BHSP_4:def 1
.= (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) by RLVECT_1:4 ; :: thesis: verum