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 <*w,v,u*>
let v, u, w be Element of V; Sum <*u,v,w*> = Sum <*w,v,u*>
thus Sum <*u,v,w*> =
Sum <*w,u,v*>
by Th68
.=
Sum <*w,v,u*>
by Th66
; verum