theorem lemma2z: :: FIELD_8:21

for F being Field
for G1, G2 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) ) & ( for i being Nat st i in dom G2 holds
ex a being Element of F st G2 . i = rpoly (1,a) ) & Product G1 = Product G2 holds
for a being Element of F 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) ) )