let F be 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) ) )
let E be 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) ) )
let G1 be non empty FinSequence of (Polynom-Ring F); ( ( for i being Nat st i in dom G1 holds
ex a being Element of F st G1 . i = rpoly (1,a) ) implies 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) ) ) )
assume AS1:
for i being Nat st i in dom G1 holds
ex a being Element of F st G1 . i = rpoly (1,a)
; 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) ) )
let G2 be non empty FinSequence of (Polynom-Ring E); ( ( 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 implies 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) ) ) )
assume AS2:
for i being Nat st i in dom G2 holds
ex a being Element of E st G2 . i = rpoly (1,a)
; ( not Product G1 = Product G2 or 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) ) ) )
assume AS3:
Product G1 = Product G2
; 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) ) )
H:
Polynom-Ring F is Subring of Polynom-Ring E
by FIELD_4:def 1;
reconsider p = Product G2 as Polynomial of E by POLYNOM3:def 10;
then
rng G1 c= the carrier of (Polynom-Ring E)
;
then reconsider G1a = G1 as non empty FinSequence of (Polynom-Ring E) by FINSEQ_1:def 4;
Product G1a = Product G2
by AS3, H, u5;
hence
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) ) )
by AS2, AS4, lemma2z; verum