let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for v, u, w being Element of V holds Sum <*v,u,w*> = (v + u) + w
let v, u, w be Element of V; :: thesis: Sum <*v,u,w*> = (v + u) + w
<*v,u,w*> = <*v,u*> ^ <*w*> by FINSEQ_1:60;
hence Sum <*v,u,w*> = (Sum <*v,u*>) + (Sum <*w*>) by Th58
.= (Sum <*v,u*>) + w by Lm6
.= (v + u) + w by Th62 ;
:: thesis: verum