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