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*>) + (Sum <*v*>)) + (Sum <*w*>)
let u, v, w be Element of V; :: thesis: Sum <*u,v,w*> = ((Sum <*u*>) + (Sum <*v*>)) + (Sum <*w*>)
thus Sum <*u,v,w*> = (u + v) + w by Th63
.= ((Sum <*u*>) + v) + w by Lm6
.= ((Sum <*u*>) + v) + (Sum <*w*>) by Lm6
.= ((Sum <*u*>) + (Sum <*v*>)) + (Sum <*w*>) by Lm6 ; :: thesis: verum