let R be Ring; :: thesis: for S being R -homomorphic Ring
for h being Homomorphism of R,S holds h . (Product (<*> the carrier of R)) = 1. S
let S be R -homomorphic Ring; :: thesis: for h being Homomorphism of R,S holds h . (Product (<*> the carrier of R)) = 1. S
let h be Homomorphism of R,S; :: thesis: h . (Product (<*> the carrier of R)) = 1. S
thus h . (Product (<*> the carrier of R)) = h . (1_ R) by GROUP_4:8
.= 1_ S by GROUP_1:def 13
.= 1. S ; :: thesis: verum