let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X holds Sum (seq,1) = (Sum (seq,0)) + (seq . 1)
let seq be sequence of X; :: thesis: Sum (seq,1) = (Sum (seq,0)) + (seq . 1)
(Partial_Sums seq) . 1 = ((Partial_Sums seq) . 0) + (seq . (0 + 1)) by BHSP_4:def 1
.= ((Partial_Sums seq) . 0) + (seq . 1) ;
hence Sum (seq,1) = (Sum (seq,0)) + (seq . 1) ; :: thesis: verum