let F be Field; :: thesis: for E being FieldExtension of F
for G being non empty FinSequence of the carrier of (Polynom-Ring F)
for q being Polynomial of F st q = Product G holds
for a being Element of E st ex i being Element of dom G ex p being Polynomial of F st
( p = G . i & Ext_eval (p,a) = 0. E ) holds
Ext_eval (q,a) = 0. E
let E be FieldExtension of F; :: thesis: for G being non empty FinSequence of the carrier of (Polynom-Ring F)
for q being Polynomial of F st q = Product G holds
for a being Element of E st ex i being Element of dom G ex p being Polynomial of F st
( p = G . i & Ext_eval (p,a) = 0. E ) holds
Ext_eval (q,a) = 0. E
let G be non empty FinSequence of the carrier of (Polynom-Ring F); :: thesis: for q being Polynomial of F st q = Product G holds
for a being Element of E st ex i being Element of dom G ex p being Polynomial of F st
( p = G . i & Ext_eval (p,a) = 0. E ) holds
Ext_eval (q,a) = 0. E
let q be Polynomial of F; :: thesis: ( q = Product G implies for a being Element of E st ex i being Element of dom G ex p being Polynomial of F st
( p = G . i & Ext_eval (p,a) = 0. E ) holds
Ext_eval (q,a) = 0. E )
assume A: q = Product G ; :: thesis: for a being Element of E st ex i being Element of dom G ex p being Polynomial of F st
( p = G . i & Ext_eval (p,a) = 0. E ) holds
Ext_eval (q,a) = 0. E
let a be Element of E; :: thesis: ( ex i being Element of dom G ex p being Polynomial of F st
( p = G . i & Ext_eval (p,a) = 0. E ) implies Ext_eval (q,a) = 0. E )
assume ex i being Element of dom G ex p being Polynomial of F st
( p = G . i & Ext_eval (p,a) = 0. E ) ; :: thesis: Ext_eval (q,a) = 0. E
then consider i being Element of dom G, p being Polynomial of F such that
B: ( p = G . i & Ext_eval (p,a) = 0. E ) ;
H: F is Subring of E by FIELD_4:def 1;
dom G = Seg (len G) by FINSEQ_1:def 3;
then ( 1 <= i & i <= len G ) by FINSEQ_1:1;
then G = ((G | (i -' 1)) ^ <*(G . i)*>) ^ (G /^ i) by FINSEQ_5:84;
then D: Product G = (Product ((G | (i -' 1)) ^ <*(G . i)*>)) * (Product (G /^ i)) by GROUP_4:5
.= ((Product (G | (i -' 1))) * (Product <*(G . i)*>)) * (Product (G /^ i)) by GROUP_4:5
.= ((Product <*(G . i)*>) * (Product (G | (i -' 1)))) * (Product (G /^ i)) by GROUP_1:def 12
.= (Product <*(G . i)*>) * ((Product (G | (i -' 1))) * (Product (G /^ i))) by GROUP_1:def 3 ;
reconsider r1 = Product (G | (i -' 1)), r2 = Product (G /^ i) as Polynomial of F by POLYNOM3:def 10;
I: G . i = G /. i by PARTFUN1:def 6;
then E: Product <*(G /. i)*> = p by B, GROUP_4:9;
r1 *' r2 = (Product (G | (i -' 1))) * (Product (G /^ i)) by POLYNOM3:def 10;
then q = p *' (r1 *' r2) by A, D, E, I, POLYNOM3:def 10;
hence Ext_eval (q,a) = (0. E) * (Ext_eval ((r1 *' r2),a)) by B, H, ALGNUM_1:20
.= 0. E ;
:: thesis: verum