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) *' (Leading-Monomial q)),x) = (Ext_eval ((Leading-Monomial p),x)) * (Ext_eval ((Leading-Monomial 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) *' (Leading-Monomial q)),x) = (Ext_eval ((Leading-Monomial p),x)) * (Ext_eval ((Leading-Monomial q),x))
let p, q be Polynomial of A; :: thesis: for x being Element of B st A is Subring of B holds
Ext_eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (Ext_eval ((Leading-Monomial p),x)) * (Ext_eval ((Leading-Monomial q),x))
let x be Element of B; :: thesis: ( A is Subring of B implies Ext_eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (Ext_eval ((Leading-Monomial p),x)) * (Ext_eval ((Leading-Monomial q),x)) )
assume A0: A is Subring of B ; :: thesis: Ext_eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (Ext_eval ((Leading-Monomial p),x)) * (Ext_eval ((Leading-Monomial q),x))

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

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

then A2: ( len q >= 0 + 1 & len p >= 0 + 1 ) by NAT_1:13;
A3: ( (len q) - 1 = (len q) -' 1 & (len p) - 1 = (len p) -' 1 ) by A1, XREAL_0:def 2;
(len p) + (len q) >= 0 + (1 + 1) by A2, XREAL_1:7;
then A4: ((len p) + (len q)) -' 2 = ((len p) + (len q)) - 2 by XREAL_1:19, XREAL_0:def 2;
A5: ((len p) + (len q)) - (1 + 1) = ((len p) - 1) + ((len q) - 1) ;
thus Ext_eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (In (((p . ((len p) -' 1)) * (q . ((len q) -' 1))),B)) * ((power B) . (x,(((len p) + (len q)) -' 2))) by A0, A1, Th20
.= (In (((p . ((len p) -' 1)) * (q . ((len q) -' 1))),B)) * (((power B) . (x,((len p) -' 1))) * ((power B) . (x,((len q) -' 1)))) by A3, A4, A5, POLYNOM2:1
.= ((In ((p . ((len p) -' 1)),B)) * (In ((q . ((len q) -' 1)),B))) * (((power B) . (x,((len p) -' 1))) * ((power B) . (x,((len q) -' 1)))) by A0, Th13
.= (In ((p . ((len p) -' 1)),B)) * ((In ((q . ((len q) -' 1)),B)) * (((power B) . (x,((len p) -' 1))) * ((power B) . (x,((len q) -' 1))))) by GROUP_1:def 3
.= (In ((p . ((len p) -' 1)),B)) * (((power B) . (x,((len p) -' 1))) * ((In ((q . ((len q) -' 1)),B)) * ((power B) . (x,((len q) -' 1))))) by GROUP_1:def 3
.= ((In ((p . ((len p) -' 1)),B)) * ((power B) . (x,((len p) -' 1)))) * ((In ((q . ((len q) -' 1)),B)) * ((power B) . (x,((len q) -' 1)))) by GROUP_1:def 3
.= ((In ((p . ((len p) -' 1)),B)) * ((power B) . (x,((len p) -' 1)))) * (Ext_eval ((Leading-Monomial q),x)) by A0, Th21
.= (Ext_eval ((Leading-Monomial p),x)) * (Ext_eval ((Leading-Monomial q),x)) by A0, Th21 ; :: thesis: verum

end;

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

then A6: Leading-Monomial p = 0_. A by POLYNOM4:12;
hence Ext_eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = Ext_eval ((0_. A),x) by POLYNOM4:2
.= (0. B) * (Ext_eval ((Leading-Monomial q),x)) by Th17
.= (Ext_eval ((Leading-Monomial p),x)) * (Ext_eval ((Leading-Monomial q),x)) by A6, Th17 ;
:: thesis: verum

end;

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

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

end;

end;