theorem :: FVSUM_1:89

for K being non empty right_complementable associative left_unital Abelian add-associative right_zeroed doubleLoopStr
for a1, a2, b1, b2 being Element of K holds <*a1,a2*> "*" <*b1,b2*> = (a1 * b1) + (a2 * b2)