let R be Ring; :: thesis: for S being RingExtension of R
for p being Element of the carrier of (Polynom-Ring R)
for q being Element of the carrier of (Polynom-Ring S) st p = q holds
deg p = deg q
let S be RingExtension of R; :: thesis: for p being Element of the carrier of (Polynom-Ring R)
for q being Element of the carrier of (Polynom-Ring S) st p = q holds
deg p = deg q
let p be Element of the carrier of (Polynom-Ring R); :: thesis: for q being Element of the carrier of (Polynom-Ring S) st p = q holds
deg p = deg q
let q be Element of the carrier of (Polynom-Ring S); :: thesis: ( p = q implies deg p = deg q )
assume A1: p = q ; :: thesis: deg p = deg q
A2: R is Subring of S by Def1;

per cases ( q is zero or not q is zero ) ;

suppose q is zero ; :: thesis: deg p = deg q

then len q = 0 by UPROOTS:17;
then A3: deg q = 0 - 1 by HURWITZ:def 2;
then q = 0_. S by HURWITZ:20
.= 0. (Polynom-Ring S) by POLYNOM3:def 10
.= 0. (Polynom-Ring R) by Th7
.= 0_. R by POLYNOM3:def 10 ;
hence deg p = deg q by A1, A3, HURWITZ:20; :: thesis: verum

end;

suppose A4: not q is zero ; :: thesis: deg p = deg q

then len q > 0 by UPROOTS:17;
then A5: (len q) -' 1 = (len q) - 1 by XREAL_0:def 2;
then reconsider lenq = (len q) - 1 as Element of NAT ;

A6: now :: thesis: for i being Nat st i >= len q holds
p . i = 0. R

let i be Nat; :: thesis: ( i >= len q implies p . i = 0. R )
assume i >= len q ; :: thesis: p . i = 0. R
then q . i = 0. S by ALGSEQ_1:8;
hence p . i = 0. R by A1, A2, C0SP1:def 3; :: thesis: verum

end;

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

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

now :: thesis: not len q > m

assume len q > m ; :: thesis: contradiction
then lenq + 1 > m ;
then lenq >= m by NAT_1:13;
then p . ((len q) -' 1) = 0. R by A5, A7, ALGSEQ_1:def 2;
then A8: q . ((len q) -' 1) = 0. S by A1, A2, C0SP1:def 3;
0 + 1 < (len q) + 1 by A4, XREAL_1:8, UPROOTS:17;
then len q >= 1 by NAT_1:13;
then ((len q) -' 1) + 1 = len q by XREAL_1:235;
hence contradiction by A8, ALGSEQ_1:10; :: thesis: verum

end;

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

end;

then len p = len q by A6, ALGSEQ_1:def 3, ALGSEQ_1:def 2;
hence deg p = (len q) - 1 by HURWITZ:def 2
.= deg q by HURWITZ:def 2 ;
:: thesis: verum

end;

end;