theorem Th54: :: RLVECT_1:54

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v, w being Element of V holds Sum <*v,w*> = Sum <*w,v*>