let R be Ring; :: thesis: for S being R -homomorphic Ring
for h being Homomorphism of R,S holds h . (Sum (<*> the carrier of R)) = 0. S
let S be R -homomorphic Ring; :: thesis: for h being Homomorphism of R,S holds h . (Sum (<*> the carrier of R)) = 0. S
let h be Homomorphism of R,S; :: thesis: h . (Sum (<*> the carrier of R)) = 0. S
thus h . (Sum (<*> the carrier of R)) = h . (0. R) by RLVECT_1:43
.= 0. S by RING_2:6 ; :: thesis: verum