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