let X be RealUnitarySpace; :: 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 Def1 ; :: thesis: verum