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