let Q, Q2 be multLoop; :: thesis: for f being homomorphic Function of Q,Q2 holds [#] (lp (Ker f)) = Ker f
let f be homomorphic Function of Q,Q2; :: thesis: [#] (lp (Ker f)) = Ker f
f . (1. Q) = 1. Q2 by Def28a;
then A1: 1. Q in Ker f by Def29;
A2: for x, y being Element of Q st x in Ker f & y in Ker f holds
x * y in Ker f

proof

let x, y be Element of Q; :: thesis: ( x in Ker f & y in Ker f implies x * y in Ker f )
assume that
A3: x in Ker f and
A4: y in Ker f ; :: thesis: x * y in Ker f
f . (x * y) = (f . x) * (f . y) by Def28b
.= (1. Q2) * (f . y) by Def29, A3
.= 1. Q2 by Def29, A4 ;
hence x * y in Ker f by Def29; :: thesis: verum

end;

A5: for x, y being Element of Q st x in Ker f & y in Ker f holds
x \ y in Ker f

proof

let x, y be Element of Q; :: thesis: ( x in Ker f & y in Ker f implies x \ y in Ker f )
assume that
A6: x in Ker f and
A7: y in Ker f ; :: thesis: x \ y in Ker f
f . (x \ y) = (f . x) \ (f . y) by Th13
.= (1. Q2) \ (f . y) by Def29, A6
.= 1. Q2 by Def29, A7 ;
hence x \ y in Ker f by Def29; :: thesis: verum

end;

for x, y being Element of Q st x in Ker f & y in Ker f holds
x / y in Ker f

proof

let x, y be Element of Q; :: thesis: ( x in Ker f & y in Ker f implies x / y in Ker f )
assume that
A8: x in Ker f and
A9: y in Ker f ; :: thesis: x / y in Ker f
f . (x / y) = (f . x) / (f . y) by Th14
.= (f . x) / (1. Q2) by Def29, A9
.= 1. Q2 by Def29, A8 ;
hence x / y in Ker f by Def29; :: thesis: verum

end;

hence [#] (lp (Ker f)) = Ker f by Th18, A1, A2, A5; :: thesis: verum