theorem Th14: :: AIMLOOP:14

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)