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