let G be Group; 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; ( 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)}
; (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 ;
( 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 )
;
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;
verum
end;
hence
(nat_hom H) | the carrier of K is one-to-one
by FUNCT_1:def 4; verum