let G, H be Group; :: thesis: for a, b being Element of G
for f being Function of the carrier of G,the carrier of H st ( for a being Element of G holds f . a = 1_ H ) holds
f . (a * b) = (f . a) * (f . b)
let a, b be Element of G; :: thesis: for f being Function of the carrier of G,the carrier of H st ( for a being Element of G holds f . a = 1_ H ) holds
f . (a * b) = (f . a) * (f . b)
let f be Function of the carrier of G,the carrier of H; :: thesis: ( ( for a being Element of G holds f . a = 1_ H ) implies f . (a * b) = (f . a) * (f . b) )
assume A1: for a being Element of G holds f . a = 1_ H ; :: thesis: f . (a * b) = (f . a) * (f . b)
hence f . (a * b) = 1_ H
.= (1_ H) * (1_ H) by GROUP_1:def 5
.= (f . a) * (1_ H) by A1
.= (f . a) * (f . b) by A1 ;
:: thesis: verum