let A be Ring; :: thesis: for B being comRing
for p, q being Polynomial of A
for x being Element of B st A is Subring of B holds
Ext_eval (((Leading-Monomial p) *' q),x) = (Ext_eval ((Leading-Monomial p),x)) * (Ext_eval (q,x))
let B be comRing; :: thesis: for p, q being Polynomial of A
for x being Element of B st A is Subring of B holds
Ext_eval (((Leading-Monomial p) *' q),x) = (Ext_eval ((Leading-Monomial p),x)) * (Ext_eval (q,x))
let p1, q be Polynomial of A; :: thesis: for x being Element of B st A is Subring of B holds
Ext_eval (((Leading-Monomial p1) *' q),x) = (Ext_eval ((Leading-Monomial p1),x)) * (Ext_eval (q,x))
let x be Element of B; :: thesis: ( A is Subring of B implies Ext_eval (((Leading-Monomial p1) *' q),x) = (Ext_eval ((Leading-Monomial p1),x)) * (Ext_eval (q,x)) )
assume A0: A is Subring of B ; :: thesis: Ext_eval (((Leading-Monomial p1) *' q),x) = (Ext_eval ((Leading-Monomial p1),x)) * (Ext_eval (q,x))
set p = Leading-Monomial p1;
defpred S₁[ Nat] means for q being Polynomial of A st len q = $1 holds
Ext_eval (((Leading-Monomial p1) *' q),x) = (Ext_eval ((Leading-Monomial p1),x)) * (Ext_eval (q,x));
A1: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume A2: for n being Nat st n < k holds
for q being Polynomial of A st len q = n holds
Ext_eval (((Leading-Monomial p1) *' q),x) = (Ext_eval ((Leading-Monomial p1),x)) * (Ext_eval (q,x)) ; :: thesis: S₁[k]
let q be Polynomial of A; :: thesis: ( len q = k implies Ext_eval (((Leading-Monomial p1) *' q),x) = (Ext_eval ((Leading-Monomial p1),x)) * (Ext_eval (q,x)) )
assume A3: len q = k ; :: thesis: Ext_eval (((Leading-Monomial p1) *' q),x) = (Ext_eval ((Leading-Monomial p1),x)) * (Ext_eval (q,x))

per cases ( len q <> 0 or len q = 0 ) ;

suppose A4: len q <> 0 ; :: thesis: Ext_eval (((Leading-Monomial p1) *' q),x) = (Ext_eval ((Leading-Monomial p1),x)) * (Ext_eval (q,x))

set LMq = Leading-Monomial q;
consider r being Polynomial of A such that
A5: len r < len q and
A6: q = r + (Leading-Monomial q) and
for n being Element of NAT st n < (len q) - 1 holds
r . n = q . n by A4, POLYNOM4:16;
thus Ext_eval (((Leading-Monomial p1) *' q),x) = Ext_eval ((((Leading-Monomial p1) *' r) + ((Leading-Monomial p1) *' (Leading-Monomial q))),x) by A6, POLYNOM3:31
.= (Ext_eval (((Leading-Monomial p1) *' r),x)) + (Ext_eval (((Leading-Monomial p1) *' (Leading-Monomial q)),x)) by A0, Th19
.= ((Ext_eval ((Leading-Monomial p1),x)) * (Ext_eval (r,x))) + (Ext_eval (((Leading-Monomial p1) *' (Leading-Monomial q)),x)) by A2, A3, A5
.= ((Ext_eval ((Leading-Monomial p1),x)) * (Ext_eval (r,x))) + ((Ext_eval ((Leading-Monomial p1),x)) * (Ext_eval ((Leading-Monomial q),x))) by A0, Th22
.= (Ext_eval ((Leading-Monomial p1),x)) * ((Ext_eval (r,x)) + (Ext_eval ((Leading-Monomial q),x))) by VECTSP_1:def 7
.= (Ext_eval ((Leading-Monomial p1),x)) * (Ext_eval (q,x)) by A0, A6, Th19 ; :: thesis: verum

end;

suppose len q = 0 ; :: thesis: Ext_eval (((Leading-Monomial p1) *' q),x) = (Ext_eval ((Leading-Monomial p1),x)) * (Ext_eval (q,x))

then A7: q = 0_. A by POLYNOM4:5;
hence Ext_eval (((Leading-Monomial p1) *' q),x) = Ext_eval ((0_. A),x) by POLYNOM3:34
.= (Ext_eval ((Leading-Monomial p1),x)) * (0. B) by Th17
.= (Ext_eval ((Leading-Monomial p1),x)) * (Ext_eval (q,x)) by A7, Th17 ;
:: thesis: verum

end;

end;

end;

A8: for n being Nat holds S₁[n] from NAT_1:sch 4(A1);
len q = len q ;
hence Ext_eval (((Leading-Monomial p1) *' q),x) = (Ext_eval ((Leading-Monomial p1),x)) * (Ext_eval (q,x)) by A8; :: thesis: verum