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