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