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)

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))

A4:
dom f = the carrier of G
by FUNCT_2:def 1;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;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

now :: thesis: for x being object st x in the carrier of (Ker (g * f)) holds

x in f " the carrier of (Ker g)

hence
the carrier of (Ker (g * f)) = f " the carrier of (Ker g)
by A1, TARSKI:2; :: thesis: verumx 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;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