let G1, G2 be Group; :: thesis: ( G2 is trivial implies for phi being Homomorphism of G1,G2 holds phi = 1: (G1,G2) )
assume A1: G2 is trivial ; :: thesis: for phi being Homomorphism of G1,G2 holds phi = 1: (G1,G2)
let phi be Homomorphism of G1,G2; :: thesis: phi = 1: (G1,G2)
multMagma(# the carrier of G2, the multF of G2 #) = (1). G2 by A1, GROUP_22:6;
then A2: the carrier of G2 = {(1_ G2)} by GROUP_2:def 7;
for g being Element of G1 holds phi . g = (1: (G1,G2)) . g

proof

let g be Element of G1; :: thesis: phi . g = (1: (G1,G2)) . g
(G1 --> (1_ G2)) . g = 1_ G2 ;
then A3: (1: (G1,G2)) . g = 1_ G2 by GROUP_6:def 7;
thus phi . g = 1_ G2 by A2, TARSKI:def 1
.= (1: (G1,G2)) . g by A3 ; :: thesis: verum

end;

hence phi = 1: (G1,G2) by FUNCT_2:def 8; :: thesis: verum