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) * (f . (x \ y)) = f . (x * (x \ y)) by Def28b;
hence f . (x \ y) = (f . x) \ (f . y) ; :: thesis: verum