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 )

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

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
h . g1 = 1_ H
; :: thesis: g1 in Ker h
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;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

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