let Q1, Q2 be multLoop; :: thesis: for f being homomorphic Function of Q1,Q2
for x, y being Element of Q1 holds f . (x / y) = (f . x) / (f . y)
let f be homomorphic Function of Q1,Q2; :: thesis: for x, y being Element of Q1 holds f . (x / y) = (f . x) / (f . y)
let x, y be Element of Q1; :: thesis: f . (x / y) = (f . x) / (f . y)
(f . (x / y)) * (f . y) = f . ((x / y) * y) by Def28b;
hence f . (x / y) = (f . x) / (f . y) ; :: thesis: verum