let R be non degenerated Ring; :: thesis: for S being R -homomorphic Ring
for h being Homomorphism of R,S
for p being non zero Element of the carrier of (Polynom-Ring R) holds
( deg ((PolyHom h) . p) = deg p iff h . (LC p) <> 0. S )
let S be R -homomorphic Ring; :: thesis: for h being Homomorphism of R,S
for p being non zero Element of the carrier of (Polynom-Ring R) holds
( deg ((PolyHom h) . p) = deg p iff h . (LC p) <> 0. S )
let h be Homomorphism of R,S; :: thesis: for p being non zero Element of the carrier of (Polynom-Ring R) holds
( deg ((PolyHom h) . p) = deg p iff h . (LC p) <> 0. S )
let p be non zero Element of the carrier of (Polynom-Ring R); :: thesis: ( deg ((PolyHom h) . p) = deg p iff h . (LC p) <> 0. S )
p <> 0_. R ;
then A1: len p <> 0 by POLYNOM4:5;

hereby :: thesis: ( h . (LC p) <> 0. S implies deg ((PolyHom h) . p) = deg p )

assume deg ((PolyHom h) . p) = deg p ; :: thesis: h . (LC p) <> 0. S
then h . (p . ((len p) -' 1)) <> 0. S by A1, Lm3;
hence h . (LC p) <> 0. S by RATFUNC1:def 6; :: thesis: verum

end;

assume h . (LC p) <> 0. S ; :: thesis: deg ((PolyHom h) . p) = deg p
then h . (p . ((len p) -' 1)) <> 0. S by RATFUNC1:def 6;
hence deg ((PolyHom h) . p) = deg p by A1, Lm3; :: thesis: verum