let H, G be Group; :: thesis: for h being Homomorphism of G,H holds
( h is one-to-one iff Ker h = (1). G )
let h be Homomorphism of G,H; :: thesis: ( h is one-to-one iff Ker h = (1). G )
thus ( h is one-to-one implies Ker h = (1). G ) :: thesis: ( Ker h = (1). G implies h is one-to-one )

proof

assume A1: h is one-to-one ; :: thesis: Ker h = (1). G

now

let x be set ; :: thesis: ( x in the carrier of (Ker h) iff x = 1_ G )
thus ( x in the carrier of (Ker h) iff x = 1_ G ) :: thesis: verum

proof

thus ( x in the carrier of (Ker h) implies x = 1_ G ) :: thesis: ( x = 1_ G implies x in the carrier of (Ker h) )

proof

assume A2: x in the carrier of (Ker h) ; :: thesis: x = 1_ G
then x in Ker h by STRUCT_0:def 5;
then x in G by GROUP_2:49;
then reconsider a = x as Element of G by STRUCT_0:def 5;
a in Ker h by A2, STRUCT_0:def 5;
then h . a = 1_ H by Th50
.= h . (1_ G) by Th40 ;
hence x = 1_ G by A1, Th1; :: thesis: verum

end;

assume A3: x = 1_ G ; :: thesis: x in the carrier of (Ker h)
then reconsider a = x as Element of G ;
h . a = 1_ H by A3, Th40;
then a in Ker h by Th50;
hence x in the carrier of (Ker h) by STRUCT_0:def 5; :: thesis: verum

end;

end;

then the carrier of (Ker h) = {(1_ G)} by TARSKI:def 1;
hence Ker h = (1). G by GROUP_2:def 7; :: thesis: verum

end;

assume Ker h = (1). G ; :: thesis: h is one-to-one
then A4: the carrier of (Ker h) = {(1_ G)} by GROUP_2:def 7;

now

let a, b be Element of G; :: thesis: ( a <> b implies not h . a = h . b )
assume that
A5: a <> b and
A6: h . a = h . b ; :: thesis: contradiction
(h . a) * (h . (a ")) = h . (a * (a ")) by Def7
.= h . (1_ G) by GROUP_1:def 6
.= 1_ H by Th40 ;
then 1_ H = h . (b * (a ")) by A6, Def7;
then b * (a ") in Ker h by Th50;
then A7: b * (a ") in the carrier of (Ker h) by STRUCT_0:def 5;
a = (1_ G) * a by GROUP_1:def 5
.= (b * (a ")) * a by A4, A7, TARSKI:def 1
.= b * ((a ") * a) by GROUP_1:def 4
.= b * (1_ G) by GROUP_1:def 6
.= b by GROUP_1:def 5 ;
hence contradiction by A5; :: thesis: verum

end;

then for a, b being Element of G st h . a = h . b holds
a = b ;
hence h is one-to-one by Th1; :: thesis: verum