let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X holds Sum (seq,1,0) = seq . 1
let seq be sequence of X; :: thesis: Sum (seq,1,0) = seq . 1
Sum (seq,1,0) = ((seq . 0) + (seq . 1)) - (Sum (seq,0)) by Th17
.= ((seq . 1) + (seq . 0)) - (seq . 0) by BHSP_4:def 1
.= (seq . 1) + ((seq . 0) - (seq . 0)) by RLVECT_1:def 3
.= (seq . 1) + H₁(X) by RLVECT_1:15 ;
hence Sum (seq,1,0) = seq . 1 by RLVECT_1:4; :: thesis: verum