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:43;
hence Sum <*v,u,w*> = (Sum <*v,u*>) + (Sum <*w*>) by Th41
.= (Sum <*v,u*>) + w by Lm6
.= (v + u) + w by Th45 ;
:: thesis: verum