let F be Field; :: thesis: 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) ) )
let G1, G2 be non empty FinSequence of (Polynom-Ring F); :: thesis: ( ( 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 implies 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) ) ) )
assume AS: ( ( 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 ) ; :: thesis: 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) ) )
let a be Element of F; :: thesis: ( 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) ) )
Product G1 is Polynomial of F by POLYNOM3:def 10;
then reconsider p1 = Product G1 as Ppoly of F by AS, RING_5:def 4;
Product G1 <> 0_. F by AS, RATFUNC1:11;
then A: not Product G1 is zero by POLYNOM3:def 10;
deg p1 <> 0 by RATFUNC1:def 2;
then B: Product G1 is NonUnit of (Polynom-Ring F) by RING_4:37;
( G1 is Factorization of Product G1 & G2 is Factorization of Product G1 ) by AS, lemma2y;
then consider B being Function of (dom G1),(dom G2) such that
C: ( B is bijective & ( for i being Element of dom G1 holds G2 . (B . i) is_associated_to G1 . i ) ) by A, B, RING_2:def 14;

X: now :: thesis: ( ex i being Nat st
( i in dom G1 & G1 . i = rpoly (1,a) ) implies ex i being Nat st
( i in dom G2 & G2 . i = rpoly (1,a) ) )

assume ex i being Nat st
( i in dom G1 & G1 . i = rpoly (1,a) ) ; :: thesis: ex i being Nat st
( i in dom G2 & G2 . i = rpoly (1,a) )
then consider i being Nat such that
X1: ( i in dom G1 & G1 . i = rpoly (1,a) ) ;
reconsider i = i as Element of dom G1 by X1;
consider j being Element of dom G1 such that
X2: G2 . (B . i) is_associated_to G1 . i by C;
consider b being Element of F such that
X3: G2 . (B . i) = rpoly (1,b) by AS;
reconsider p1 = G1 . i, p2 = G2 . (B . i) as Element of the carrier of (Polynom-Ring F) ;
thus ex i being Nat st
( i in dom G2 & G2 . i = rpoly (1,a) ) by X1, X2, X3, RING_4:30; :: thesis: verum

end;

now :: thesis: ( ex i being Nat st
( i in dom G2 & G2 . i = rpoly (1,a) ) implies ex i being Nat st
( i in dom G1 & G1 . i = rpoly (1,a) ) )

assume ex i being Nat st
( i in dom G2 & G2 . i = rpoly (1,a) ) ; :: thesis: ex i being Nat st
( i in dom G1 & G1 . i = rpoly (1,a) )
then consider i being Nat such that
X1: ( i in dom G2 & G2 . i = rpoly (1,a) ) ;
reconsider i = i as Element of dom G2 by X1;
X2: ( B is one-to-one & B is onto ) by C;
reconsider C = B " as Function of (dom G2),(dom G1) by X2, FUNCT_2:25;
C . i in dom G1 ;
then reconsider j = (B ") . i as Element of dom G1 ;
X3: G2 . (B . j) is_associated_to G1 . j by C;
consider b being Element of F such that
X4: G1 . j = rpoly (1,b) by AS;
reconsider p1 = G1 . j, p2 = G2 . i as Element of the carrier of (Polynom-Ring F) ;
i = B . j by X2, FUNCT_1:35;
hence ex i being Nat st
( i in dom G1 & G1 . i = rpoly (1,a) ) by X1, X4, X3, RING_4:30; :: thesis: verum

end;

hence ( 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) ) ) by X; :: thesis: verum