let V be non empty add-associative right_zeroed left_zeroed addLoopStr ; :: thesis: for v, u being Element of V holds Sum <*v,u*> = v + u
let v, u be Element of V; :: thesis: Sum <*v,u*> = v + u
<*v,u*> = <*v*> ^ <*u*> by FINSEQ_1:def 9;
then Sum <*v,u*> = (Sum <*v*>) + (Sum <*u*>) by RLVECT_1:41
.= v + (Sum <*u*>) by BINOM:3
.= v + u by BINOM:3 ;
hence Sum <*v,u*> = v + u ; :: thesis: verum