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 * (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 * (Ker f) iff f . x = f . y )
let x, y be Element of Q; :: thesis: ( y in x * (Ker f) iff f . x = f . y )
thus ( y in x * (Ker f) implies f . x = f . y ) :: thesis: ( f . x = f . y implies y in x * (Ker f) )

proof

assume y in x * (Ker f) ; :: thesis: f . x = f . y
then consider h being Permutation of Q such that
A1: ( h in Mlt (Ker f) & y = h . x ) by Def39;
f . x = (f * h) . x by Th45, A1
.= f . y by A1, FUNCT_2:15 ;
hence f . x = f . y ; :: thesis: verum

end;

assume A2: f . x = f . y ; :: thesis: y in x * (Ker f)
ex h being Permutation of Q st
( h in Mlt (Ker f) & y = h . x )

proof

reconsider h = (curry the multF of Q) . (y / x) as Permutation of Q by Th30;
take h ; :: thesis: ( h in Mlt (Ker f) & y = h . x )
f . (y / x) = (f . y) / (f . x) by Th14
.= 1. Q2 by Th6, A2 ;
then A3: y / x in Ker f by Def29;
h . x = (y / x) * x by FUNCT_5:69
.= y ;
hence ( h in Mlt (Ker f) & y = h . x ) by A3, Th32; :: thesis: verum

end;

hence y in x * (Ker f) by Def39; :: thesis: verum