let G1, G2 be Group; :: thesis: for f being Homomorphism of G1,G2
for H being Subgroup of G1 holds Ker (f | H) is Subgroup of Ker f
let f be Homomorphism of G1,G2; :: thesis: for H being Subgroup of G1 holds Ker (f | H) is Subgroup of Ker f
let H be Subgroup of G1; :: thesis: Ker (f | H) is Subgroup of Ker f
A1: Ker (f | H) is Subgroup of G1 by GROUP_2:56;
for g being Element of G1 st g in Ker (f | H) holds
g in Ker f

proof

let g be Element of G1; :: thesis: ( g in Ker (f | H) implies g in Ker f )
assume A2: g in Ker (f | H) ; :: thesis: g in Ker f
then A3: g in H by GROUP_2:40;
(f | H) . g = f . g by A2, Th1, GROUP_2:40;
then 1_ G2 = f . g by A2, A3, GROUP_6:41;
hence g in Ker f by GROUP_6:41; :: thesis: verum

end;

hence Ker (f | H) is Subgroup of Ker f by A1, GROUP_2:58; :: thesis: verum