let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for n being Element of NAT holds seq . (n + 1) = (Sum seq,(n + 1)) - (Sum seq,n)
let seq be sequence of X; :: thesis: for n being Element of NAT holds seq . (n + 1) = (Sum seq,(n + 1)) - (Sum seq,n)
let n be Element of 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 6
.= (seq . (n + 1)) + (0. X) by RLVECT_1:28
.= seq . (n + 1) by RLVECT_1:10 ; :: thesis: verum