let G, H be Group; :: thesis: for a being Element of G
for h being Homomorphism of G,H holds
( a in Ker h iff h . a = 1_ H )
let a be Element of G; :: thesis: for h being Homomorphism of G,H holds
( a in Ker h iff h . a = 1_ H )
let h be Homomorphism of G,H; :: thesis: ( a in Ker h iff h . a = 1_ H )
thus ( a in Ker h implies h . a = 1_ H ) :: thesis: ( h . a = 1_ H implies a in Ker h )

proof

assume a in Ker h ; :: thesis: h . a = 1_ H
then a in the carrier of (Ker h) ;
then a in { b where b is Element of G : h . b = 1_ H } by Def9;
then ex b being Element of G st
( a = b & h . b = 1_ H ) ;
hence h . a = 1_ H ; :: thesis: verum

end;

assume h . a = 1_ H ; :: thesis: a in Ker h
then a in { b where b is Element of G : h . b = 1_ H } ;
then a in the carrier of (Ker h) by Def9;
hence a in Ker h ; :: thesis: verum