A1: the carrier of A c= the carrier of G by GROUP_2:def 5;
then reconsider f = g | the carrier of A as Function of the carrier of A, the carrier of H by FUNCT_2:32;
now :: thesis: for a, b being Element of A holds (f . a) * (f . b) = f . (a * b)
A2: for a, b being Element of G holds the multF of H . ((g . a),(g . b)) = g . ( the multF of G . (a,b))
proof
let a, b be Element of G; :: thesis: the multF of H . ((g . a),(g . b)) = g . ( the multF of G . (a,b))
thus the multF of H . ((g . a),(g . b)) = (g . a) * (g . b)
.= g . (a * b) by GROUP_6:def 6
.= g . ( the multF of G . (a,b)) ; :: thesis: verum
end;
let a, b be Element of A; :: thesis: (f . a) * (f . b) = f . (a * b)
A3: ( f . a = g . a & f . b = g . b ) by FUNCT_1:49;
A4: the multF of G . (a,b) = a * b
proof
reconsider b9 = b as Element of G by A1;
reconsider a9 = a as Element of G by A1;
thus the multF of G . (a,b) = a9 * b9
.= a * b by GROUP_2:43 ; :: thesis: verum
end;
( a is Element of G & b is Element of G ) by A1;
hence (f . a) * (f . b) = g . ( the multF of G . (a,b)) by A3, A2
.= f . (a * b) by A4, FUNCT_1:49 ;
:: thesis: verum
end;
hence g | the carrier of A is Homomorphism of A,H by GROUP_6:def 6; :: thesis: verum