let O be set ; :: thesis: for G, H being GroupWithOperators of O

for g being Homomorphism of G,H holds g . (1_ G) = 1_ H

let G, H be GroupWithOperators of O; :: thesis: for g being Homomorphism of G,H holds g . (1_ G) = 1_ H

let g be Homomorphism of G,H; :: thesis: g . (1_ G) = 1_ H

g . (1_ G) = g . ((1_ G) * (1_ G)) by GROUP_1:def 4

.= (g . (1_ G)) * (g . (1_ G)) by GROUP_6:def 6 ;

hence g . (1_ G) = 1_ H by GROUP_1:7; :: thesis: verum

for g being Homomorphism of G,H holds g . (1_ G) = 1_ H

let G, H be GroupWithOperators of O; :: thesis: for g being Homomorphism of G,H holds g . (1_ G) = 1_ H

let g be Homomorphism of G,H; :: thesis: g . (1_ G) = 1_ H

g . (1_ G) = g . ((1_ G) * (1_ G)) by GROUP_1:def 4

.= (g . (1_ G)) * (g . (1_ G)) by GROUP_6:def 6 ;

hence g . (1_ G) = 1_ H by GROUP_1:7; :: thesis: verum