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) st len p <> 0 holds
( len ((PolyHom h) . p) = len p iff h . (p . ((len p) -' 1)) <> 0. S )
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) st len p <> 0 holds
( len ((PolyHom h) . p) = len p iff h . (p . ((len p) -' 1)) <> 0. S )
let h be Homomorphism of R,S; :: thesis: for p being Element of the carrier of (Polynom-Ring R) st len p <> 0 holds
( len ((PolyHom h) . p) = len p iff h . (p . ((len p) -' 1)) <> 0. S )
let p be Element of the carrier of (Polynom-Ring R); :: thesis: ( len p <> 0 implies ( len ((PolyHom h) . p) = len p iff h . (p . ((len p) -' 1)) <> 0. S ) )
set lp1 = (len p) -' 1;
assume len p <> 0 ; :: thesis: ( len ((PolyHom h) . p) = len p iff h . (p . ((len p) -' 1)) <> 0. S )
then A2: (len p) - 1 = (len p) -' 1 by XREAL_0:def 2;
then A3: ((len p) -' 1) + 1 = len p ;
A4: len ((PolyHom h) . p) <= len p by Lm2;

A5: now :: thesis: ( h . (p . ((len p) -' 1)) <> 0. S implies len ((PolyHom h) . p) = len p )

assume h . (p . ((len p) -' 1)) <> 0. S ; :: thesis: len ((PolyHom h) . p) = len p
then A6: ((PolyHom h) . p) . ((len p) -' 1) <> 0. S by Def2;

now :: thesis: not len ((PolyHom h) . p) < len p

assume len ((PolyHom h) . p) < len p ; :: thesis: contradiction
then len ((PolyHom h) . p) <= (len p) -' 1 by A3, NAT_1:13;
hence contradiction by A6, ALGSEQ_1:8; :: thesis: verum

end;

hence len ((PolyHom h) . p) = len p by A4, XXREAL_0:1; :: thesis: verum

end;

now :: thesis: ( len ((PolyHom h) . p) = len p implies h . (p . ((len p) -' 1)) <> 0. S )

assume len ((PolyHom h) . p) = len p ; :: thesis: h . (p . ((len p) -' 1)) <> 0. S
then len ((PolyHom h) . p) = ((len p) -' 1) + 1 by A2;
then ((PolyHom h) . p) . ((len p) -' 1) <> 0. S by ALGSEQ_1:10;
hence h . (p . ((len p) -' 1)) <> 0. S by Def2; :: thesis: verum

end;

hence ( len ((PolyHom h) . p) = len p iff h . (p . ((len p) -' 1)) <> 0. S ) by A5; :: thesis: verum