let R be Ring; :: thesis: for S being R -homomorphic Ring
for h being Homomorphism of R,S
for a being Element of R holds (PolyHom h) . (a | R) = (h . a) | S
let S be R -homomorphic Ring; :: thesis: for h being Homomorphism of R,S
for a being Element of R holds (PolyHom h) . (a | R) = (h . a) | S
let h be Homomorphism of R,S; :: thesis: for a being Element of R holds (PolyHom h) . (a | R) = (h . a) | S
let a be Element of R; :: thesis: (PolyHom h) . (a | R) = (h . a) | S
reconsider g = a | R as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
now :: thesis: for i being Element of NAT holds ((PolyHom h) . g) . i = ((h . a) | S) . i
let i be Element of NAT ; :: thesis: ((PolyHom h) . g) . b1 = ((h . a) | S) . b1
per cases ( i <> 0 or i = 0 ) ;
suppose A: i <> 0 ; :: thesis: ((PolyHom h) . g) . b1 = ((h . a) | S) . b1
thus ((PolyHom h) . g) . i = h . (g . i) by FIELD_1:def 2
.= h . (0. R) by A, poly0
.= 0. S by RING_2:6
.= ((h . a) | S) . i by A, poly0 ; :: thesis: verum
end;
suppose B: i = 0 ; :: thesis: ((PolyHom h) . g) . b1 = ((h . a) | S) . b1
thus ((PolyHom h) . g) . i = h . (g . i) by FIELD_1:def 2
.= h . a by B, poly0
.= ((h . a) | S) . i by B, poly0 ; :: thesis: verum
end;
end;
end;
hence (PolyHom h) . (a | R) = (h . a) | S by FUNCT_2:63; :: thesis: verum