theorem Th13: :: AIMLOOP:13

for Q1, Q2 being multLoop
for f being homomorphic Function of Q1,Q2
for x, y being Element of Q1 holds f . (x \ y) = (f . x) \ (f . y)