let Q, Q2 be multLoop; :: thesis: for f being homomorphic Function of Q,Q2
for x, y being Element of Q holds
( x * (lp (Ker f)) = y * (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
( x * (lp (Ker f)) = y * (lp (Ker f)) iff f . x = f . y )
A1: for x, y being Element of Q st f . x = f . y holds
x * (lp (Ker f)) c= y * (lp (Ker f))

proof

let x, y be Element of Q; :: thesis: ( f . x = f . y implies x * (lp (Ker f)) c= y * (lp (Ker f)) )
assume A2: f . x = f . y ; :: thesis: x * (lp (Ker f)) c= y * (lp (Ker f))
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in x * (lp (Ker f)) or z in y * (lp (Ker f)) )
assume A3: z in x * (lp (Ker f)) ; :: thesis: z in y * (lp (Ker f))
then f . x = f . z by Th47;
hence z in y * (lp (Ker f)) by A3, A2, Th47; :: thesis: verum

end;

let x, y be Element of Q; :: thesis: ( x * (lp (Ker f)) = y * (lp (Ker f)) iff f . x = f . y )
( x * (lp (Ker f)) = y * (lp (Ker f)) implies f . x = f . y )

proof

assume A4: x * (lp (Ker f)) = y * (lp (Ker f)) ; :: thesis: f . x = f . y
f . y = f . y ;
then y in y * (lp (Ker f)) by Th47;
hence f . x = f . y by A4, Th47; :: thesis: verum

end;

hence ( x * (lp (Ker f)) = y * (lp (Ker f)) iff f . x = f . y ) by A1; :: thesis: verum