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

proof

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

end;

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