let V be non empty right_complementable add-associative right_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;
hence Sum <*v,u*> = (Sum <*v*>) + (Sum <*u*>) by Th41
.= v + (Sum <*u*>) by Lm6
.= v + u by Lm6 ;
:: thesis: verum