let G1, G2, G3 be Group; :: thesis: for f1 being Homomorphism of G1,G2
for f2 being Homomorphism of G2,G3 holds the carrier of (Ker (f2 * f1)) = f1 " the carrier of (Ker f2)
let f1 be Homomorphism of G1,G2; :: thesis: for f2 being Homomorphism of G2,G3 holds the carrier of (Ker (f2 * f1)) = f1 " the carrier of (Ker f2)
let f2 be Homomorphism of G2,G3; :: thesis: the carrier of (Ker (f2 * f1)) = f1 " the carrier of (Ker f2)
A1: ( f1 " the carrier of (Ker f2) is Subset of G1 & the carrier of (Ker (f2 * f1)) is Subset of G1 ) by GROUP_2:def 5, FUNCT_2:39;
for g being Element of G1 st g in the carrier of (Ker (f2 * f1)) holds
g in f1 " the carrier of (Ker f2)

proof

let g be Element of G1; :: thesis: ( g in the carrier of (Ker (f2 * f1)) implies g in f1 " the carrier of (Ker f2) )
assume g in the carrier of (Ker (f2 * f1)) ; :: thesis: g in f1 " the carrier of (Ker f2)
then g in Ker (f2 * f1) ;
then f1 . g in Ker f2 by Th44;
hence g in f1 " the carrier of (Ker f2) by FUNCT_2:38; :: thesis: verum

end;

then A2: the carrier of (Ker (f2 * f1)) c= f1 " the carrier of (Ker f2) by A1, SUBSET_1:2;
for g being Element of G1 st g in f1 " the carrier of (Ker f2) holds
g in the carrier of (Ker (f2 * f1))

proof

let g be Element of G1; :: thesis: ( g in f1 " the carrier of (Ker f2) implies g in the carrier of (Ker (f2 * f1)) )
assume g in f1 " the carrier of (Ker f2) ; :: thesis: g in the carrier of (Ker (f2 * f1))
then f1 . g in Ker f2 by FUNCT_2:38;
then g in Ker (f2 * f1) by Th44;
hence g in the carrier of (Ker (f2 * f1)) ; :: thesis: verum

end;

then A3: f1 " the carrier of (Ker f2) c= the carrier of (Ker (f2 * f1)) by A1, SUBSET_1:2;
thus the carrier of (Ker (f2 * f1)) = f1 " the carrier of (Ker f2) by A2, A3, XBOOLE_0:def 10; :: thesis: verum