let O be set ; :: thesis: for G, H, I being GroupWithOperators of O
for f being Homomorphism of G,H
for g being Homomorphism of H,I holds the carrier of (Ker (g * f)) = f " the carrier of (Ker g)
let G, H, I be GroupWithOperators of O; :: thesis: for f being Homomorphism of G,H
for g being Homomorphism of H,I holds the carrier of (Ker (g * f)) = f " the carrier of (Ker g)
let f be Homomorphism of G,H; :: thesis: for g being Homomorphism of H,I holds the carrier of (Ker (g * f)) = f " the carrier of (Ker g)
let g be Homomorphism of H,I; :: thesis: the carrier of (Ker (g * f)) = f " the carrier of (Ker g)
A1: now :: thesis: for x being object st x in f " the carrier of (Ker g) holds
x in the carrier of (Ker (g * f))
let x be object ; :: thesis: ( x in f " the carrier of (Ker g) implies x in the carrier of (Ker (g * f)) )
assume A2: x in f " the carrier of (Ker g) ; :: thesis: x in the carrier of (Ker (g * f))
then f . x in the carrier of (Ker g) by FUNCT_1:def 7;
then f . x in { b where b is Element of H : g . b = 1_ I } by Def21;
then A3: ex b being Element of H st
( b = f . x & g . b = 1_ I ) ;
x in dom f by A2, FUNCT_1:def 7;
then 1_ I = (g * f) . x by A3, FUNCT_1:13;
then x in { a9 where a9 is Element of G : (g * f) . a9 = 1_ I } by A2;
hence x in the carrier of (Ker (g * f)) by Def21; :: thesis: verum
end;
A4: dom f = the carrier of G by FUNCT_2:def 1;
now :: thesis: for x being object st x in the carrier of (Ker (g * f)) holds
x in f " the carrier of (Ker g)
let x be object ; :: thesis: ( x in the carrier of (Ker (g * f)) implies x in f " the carrier of (Ker g) )
assume x in the carrier of (Ker (g * f)) ; :: thesis: x in f " the carrier of (Ker g)
then x in { a where a is Element of G : (g * f) . a = 1_ I } by Def21;
then consider a being Element of G such that
A5: x = a and
A6: (g * f) . a = 1_ I ;
reconsider b = f . a as Element of H ;
g . b = 1_ I by A4, A6, FUNCT_1:13;
then f . x in { b9 where b9 is Element of H : g . b9 = 1_ I } by A5;
then f . x in the carrier of (Ker g) by Def21;
hence x in f " the carrier of (Ker g) by A4, A5, FUNCT_1:def 7; :: thesis: verum
end;
hence the carrier of (Ker (g * f)) = f " the carrier of (Ker g) by A1, TARSKI:2; :: thesis: verum