let G, H be non empty unital multMagma ; :: thesis: for f being Function of G,H st ( for a being Element of G holds f . a = 1_ H ) holds
for a, b being Element of G holds f . (a * b) = (f . a) * (f . b)
let f be Function of G,H; :: thesis: ( ( for a being Element of G holds f . a = 1_ H ) implies for a, b being Element of G holds f . (a * b) = (f . a) * (f . b) )
assume A1: for a being Element of G holds f . a = 1_ H ; :: thesis: for a, b being Element of G holds f . (a * b) = (f . a) * (f . b)
let a, b be Element of G; :: thesis: f . (a * b) = (f . a) * (f . b)
thus f . (a * b) = 1_ H by A1
.= (1_ H) * (1_ H) by GROUP_1:def 4
.= (f . a) * (1_ H) by A1
.= (f . a) * (f . b) by A1 ; :: thesis: verum