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