let R be Ring; :: thesis: for S being R -homomorphic Ring
for h being Homomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R)
for b being Element of R holds (PolyHom h) . (b * p) = (h . b) * ((PolyHom h) . p)
let S be R -homomorphic Ring; :: thesis: for h being Homomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R)
for b being Element of R holds (PolyHom h) . (b * p) = (h . b) * ((PolyHom h) . p)
let h be Homomorphism of R,S; :: thesis: for p being Element of the carrier of (Polynom-Ring R)
for b being Element of R holds (PolyHom h) . (b * p) = (h . b) * ((PolyHom h) . p)
let p be Element of the carrier of (Polynom-Ring R); :: thesis: for b being Element of R holds (PolyHom h) . (b * p) = (h . b) * ((PolyHom h) . p)
let b be Element of R; :: thesis: (PolyHom h) . (b * p) = (h . b) * ((PolyHom h) . p)
reconsider q = b * p as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
reconsider f = (PolyHom h) . q as Element of the carrier of (Polynom-Ring S) ;
now :: thesis: for i being Element of NAT holds f . i = ((h . b) * ((PolyHom h) . p)) . i
let i be Element of NAT ; :: thesis: f . i = ((h . b) * ((PolyHom h) . p)) . i
f . i = h . (q . i) by Def2
.= h . (b * (p . i)) by POLYNOM5:def 4
.= (h . b) * (h . (p . i)) by GROUP_6:def 6
.= (h . b) * (((PolyHom h) . p) . i) by Def2
.= ((h . b) * ((PolyHom h) . p)) . i by POLYNOM5:def 4 ;
hence f . i = ((h . b) * ((PolyHom h) . p)) . i ; :: thesis: verum
end;
hence (PolyHom h) . (b * p) = (h . b) * ((PolyHom h) . p) by FUNCT_2:63; :: thesis: verum