let n be Element of 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 6
.= (seq . (n + 1)) + (0. X) by RLVECT_1:28
.= seq . (n + 1) by RLVECT_1:10 ; :: thesis: verum