let Q, Q2 be multLoop; :: thesis: for f being homomorphic Function of Q,Q2
for x, y being Element of Q holds
( y in x * (lp (Ker f)) iff f . x = f . y )
let f be homomorphic Function of Q,Q2; :: thesis: for x, y being Element of Q holds
( y in x * (lp (Ker f)) iff f . x = f . y )
let x, y be Element of Q; :: thesis: ( y in x * (lp (Ker f)) iff f . x = f . y )
( y in x * (lp (Ker f)) iff y in x * (Ker f) ) by Th19;
hence ( y in x * (lp (Ker f)) iff f . x = f . y ) by Th46; :: thesis: verum