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) holds len ((PolyHom h) . p) <= len 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) holds len ((PolyHom h) . p) <= len p
let h be Homomorphism of R,S; :: thesis: for p being Element of the carrier of (Polynom-Ring R) holds len ((PolyHom h) . p) <= len p
let p be Element of the carrier of (Polynom-Ring R); :: thesis: len ((PolyHom h) . p) <= len p
reconsider f = (PolyHom h) . p as Element of the carrier of (Polynom-Ring S) ;

now :: thesis: for i being Nat st i >= len p holds
f . i = 0. S

let i be Nat; :: thesis: ( i >= len p implies f . i = 0. S )
assume i >= len p ; :: thesis: f . i = 0. S
then p . i = 0. R by ALGSEQ_1:8;
hence f . i = h . (0. R) by Def2
.= 0. S by RING_2:6 ;
:: thesis: verum

end;

then len p is_at_least_length_of f ;
hence len ((PolyHom h) . p) <= len p by ALGSEQ_1:def 3; :: thesis: verum