take the carrier of G --> (1_ H) ; :: thesis: for a being Element of G holds ( the carrier of G --> (1_ H)) . a = 1_ H
thus for a being Element of G holds ( the carrier of G --> (1_ H)) . a = 1_ H by FUNCOP_1:7; :: thesis: verum