let G1, G2, G3 be Group; :: thesis: for f1 being Homomorphism of G1,G2
for f2 being Homomorphism of G2,G3
for g being Element of G1 holds
( g in Ker (f2 * f1) iff f1 . g in Ker f2 )
let f1 be Homomorphism of G1,G2; :: thesis: for f2 being Homomorphism of G2,G3
for g being Element of G1 holds
( g in Ker (f2 * f1) iff f1 . g in Ker f2 )
let f2 be Homomorphism of G2,G3; :: thesis: for g being Element of G1 holds
( g in Ker (f2 * f1) iff f1 . g in Ker f2 )
let g be Element of G1; :: thesis: ( g in Ker (f2 * f1) iff f1 . g in Ker f2 )
thus ( g in Ker (f2 * f1) implies f1 . g in Ker f2 ) :: thesis: ( f1 . g in Ker f2 implies g in Ker (f2 * f1) )

proof

assume g in Ker (f2 * f1) ; :: thesis: f1 . g in Ker f2
then 1_ G3 = (f2 * f1) . g by GROUP_6:41
.= f2 . (f1 . g) by FUNCT_2:15 ;
hence f1 . g in Ker f2 by GROUP_6:41; :: thesis: verum

end;

thus ( f1 . g in Ker f2 implies g in Ker (f2 * f1) ) :: thesis: verum

proof

assume f1 . g in Ker f2 ; :: thesis: g in Ker (f2 * f1)
then 1_ G3 = f2 . (f1 . g) by GROUP_6:41
.= (f2 * f1) . g by FUNCT_2:15 ;
hence g in Ker (f2 * f1) by GROUP_6:41; :: thesis: verum

end;