let X be RealUnitarySpace; :: 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 Th18
.= ((seq . 1) + (seq . 0 )) - (seq . 0 ) by Def1
.= (seq . 1) + ((seq . 0 ) - (seq . 0 )) by RLVECT_1:def 6
.= (seq . 1) + H₁(X) by RLVECT_1:28 ;
hence Sum seq,1,0 = seq . 1 by RLVECT_1:10; :: thesis: verum