theorem lemNor1b: :: FIELD_13:4

for F being Field
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