let R be Ring; :: thesis: for S being R -homomorphic R -monomorphic Ring
for h being Monomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R) holds deg ((PolyHom h) . p) = deg p
let S be R -homomorphic R -monomorphic Ring; :: thesis: for h being Monomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R) holds deg ((PolyHom h) . p) = deg p
let h be Monomorphism of R,S; :: thesis: for p being Element of the carrier of (Polynom-Ring R) holds deg ((PolyHom h) . p) = deg p
let p be Element of the carrier of (Polynom-Ring R); :: thesis: deg ((PolyHom h) . p) = deg p
reconsider f = (PolyHom h) . p as Element of the carrier of (Polynom-Ring S) ;

A1: 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;

now :: thesis: for m being Nat st m is_at_least_length_of f holds
len p <= m

let m be Nat; :: thesis: ( m is_at_least_length_of f implies len p <= m )
assume A2: m is_at_least_length_of f ; :: thesis: len p <= m

now :: thesis: not len p > m

assume len p > m ; :: thesis: contradiction
then (len p) - 1 > m - 1 by XREAL_1:6;
then A3: (len p) - 1 >= (m - 1) + 1 by INT_1:7;
then reconsider lp = (len p) - 1 as Element of NAT by INT_1:3;
A4: lp + 1 = len p ;
h . (0. R) = 0. S by RING_2:6
.= f . lp by A3, A2
.= h . (p . lp) by Def2 ;
then p . lp = 0. R by FUNCT_2:19;
hence contradiction by A4, ALGSEQ_1:10; :: thesis: verum

end;

hence len p <= m ; :: thesis: verum

end;

hence deg ((PolyHom h) . p) = deg p by A1, ALGSEQ_1:def 2, ALGSEQ_1:def 3; :: thesis: verum