let G, H 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 :: thesis: for x being object holds
( x in the carrier of (Ker h) iff x = 1_ G )

let x be object ; :: 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 ;
then x in G by GROUP_2:40;
then reconsider a = x as Element of G ;
a in Ker h by A2;
then h . a = 1_ H by Th41
.= h . (1_ G) by Th31 ;
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, Th31;
then a in Ker h by Th41;
hence x in the carrier of (Ker h) ; :: 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 :: thesis: for a, b being Element of G st a <> b holds
not h . a = h . b

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 Def6
.= h . (1_ G) by GROUP_1:def 5
.= 1_ H by Th31 ;
then 1_ H = h . (b * (a ")) by A6, Def6;
then b * (a ") in Ker h by Th41;
then A7: b * (a ") in the carrier of (Ker h) ;
a = (1_ G) * a by GROUP_1:def 4
.= (b * (a ")) * a by A4, A7, TARSKI:def 1
.= b * ((a ") * a) by GROUP_1:def 3
.= b * (1_ G) by GROUP_1:def 5
.= b by GROUP_1:def 4 ;
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