for F being Field
for E being FieldExtension of F
for G1 being non empty FinSequence of (Polynom-Ring F) st ( for i being Nat st i in dom G1 holds
ex a being Element of F st G1 . i = rpoly (1,a) ) holds
for G2 being non empty FinSequence of (Polynom-Ring E) st ( for i being Nat st i in dom G2 holds
ex a being Element of E st G2 . i = rpoly (1,a) ) & Product G1 = Product G2 holds
for a being Element of E holds
( ex i being Nat st
( i in dom G1 & G1 . i = rpoly (1,a) ) iff ex i being Nat st
( i in dom G2 & G2 . i = rpoly (1,a) ) )