let G be Group; :: thesis: for H, K being normal Subgroup of G st the carrier of H /\ the carrier of K = {(1_ G)} holds
(nat_hom H) | the carrier of K is one-to-one
let H, K be normal Subgroup of G; :: thesis: ( the carrier of H /\ the carrier of K = {(1_ G)} implies (nat_hom H) | the carrier of K is one-to-one )
assume AS1: the carrier of H /\ the carrier of K = {(1_ G)} ; :: thesis: (nat_hom H) | the carrier of K is one-to-one
set f = nat_hom H;
set g = (nat_hom H) | the carrier of K;
for x1, x2 being object st x1 in dom ((nat_hom H) | the carrier of K) & x2 in dom ((nat_hom H) | the carrier of K) & ((nat_hom H) | the carrier of K) . x1 = ((nat_hom H) | the carrier of K) . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom ((nat_hom H) | the carrier of K) & x2 in dom ((nat_hom H) | the carrier of K) & ((nat_hom H) | the carrier of K) . x1 = ((nat_hom H) | the carrier of K) . x2 implies x1 = x2 )
assume AS2: ( x1 in dom ((nat_hom H) | the carrier of K) & x2 in dom ((nat_hom H) | the carrier of K) & ((nat_hom H) | the carrier of K) . x1 = ((nat_hom H) | the carrier of K) . x2 ) ; :: thesis: x1 = x2
then A1: ( x1 in the carrier of K & x1 in dom (nat_hom H) ) by RELAT_1:57;
reconsider y1 = x1 as Element of G by AS2;
A2: ( x2 in the carrier of K & x2 in dom (nat_hom H) ) by AS2, RELAT_1:57;
reconsider y2 = x2 as Element of G by AS2;
A3: y1 * H = (nat_hom H) . y1 by GROUP_6:def 8
.= ((nat_hom H) | the carrier of K) . x1 by A1, FUNCT_1:49
.= (nat_hom H) . y2 by AS2, A2, FUNCT_1:49
.= y2 * H by GROUP_6:def 8 ;
y1 * (1_ G) in y1 * H by GROUP_2:46, GROUP_2:103;
then y1 in y2 * H by A3, GROUP_1:def 4;
then consider h being Element of G such that
A4: ( y1 = y2 * h & h in H ) by GROUP_2:103;
( y1 in K & y2 in K ) by AS2, RELAT_1:57;
then ( y1 in K & y2 " in K ) by GROUP_2:51;
then A6: (y2 ") * y1 in K by GROUP_2:50;
(y2 ") * y1 in the carrier of H by A4, GROUP_1:13;
then (y2 ") * y1 in {(1_ G)} by AS1, XBOOLE_0:def 4, A6;
then (y2 ") * y1 = 1_ G by TARSKI:def 1;
then y2 " = y1 " by GROUP_1:12;
hence x1 = x2 by GROUP_1:9; :: thesis: verum

end;

hence (nat_hom H) | the carrier of K is one-to-one by FUNCT_1:def 4; :: thesis: verum