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

(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

hence
(nat_hom H) | the carrier of K is one-to-one
by FUNCT_1:def 4; :: thesis: verum
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;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