let F be Field; :: thesis: 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; :: thesis: 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); :: thesis: ( ( 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) ; :: thesis: 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); :: thesis: ( ( 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) ; :: thesis: ( 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 ; :: thesis: 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;
now :: thesis: for o being object st o in rng G1 holds
o in the carrier of (Polynom-Ring E)
let o be object ; :: thesis: ( o in rng G1 implies o in the carrier of (Polynom-Ring E) )
assume o in rng G1 ; :: thesis: o in the carrier of (Polynom-Ring E)
then consider i being object such that
H1: ( i in dom G1 & G1 . i = o ) by FUNCT_1:def 3;
reconsider i = i as Nat by H1;
consider a being Element of F such that
H2: G1 . i = rpoly (1,a) by H1, AS1;
F is Subring of E by FIELD_4:def 1;
then the carrier of F c= the carrier of E by C0SP1:def 3;
then reconsider b = a as Element of E ;
rpoly (1,a) = rpoly (1,b) by FIELD_4:21;
hence o in the carrier of (Polynom-Ring E) by H1, H2, POLYNOM3:def 10; :: thesis: verum
end;
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;
AS4: now :: thesis: for i being Nat st i in dom G1a holds
ex a being Element of E st G1a . i = rpoly (1,a)
let i be Nat; :: thesis: ( i in dom G1a implies ex a being Element of E st G1a . i = rpoly (1,a) )
assume i in dom G1a ; :: thesis: ex a being Element of E st G1a . i = rpoly (1,a)
then consider a being Element of F such that
L: G1 . i = rpoly (1,a) by AS1;
F is Subring of E by FIELD_4:def 1;
then the carrier of F c= the carrier of E by C0SP1:def 3;
then reconsider b = a as Element of E ;
rpoly (1,a) = rpoly (1,b) by FIELD_4:21;
hence ex a being Element of E st G1a . i = rpoly (1,a) by L; :: thesis: verum
end;
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; :: thesis: verum