theorem :: FVSUM_1:88

for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for a, b being Element of K holds <*a*> "*" <*b*> = a * b