let n be non zero Nat; :: thesis: for F being non almost_trivial Field ex K being non polynomial_disjoint Field ex p being Polynomial of K st
( K,F are_isomorphic & deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )
let F be non almost_trivial Field; :: thesis: ex K being non polynomial_disjoint Field ex p being Polynomial of K st
( K,F are_isomorphic & deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )
set x = the non trivial Element of F;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
reconsider o = rpoly (n,(0. F)) as object ;
set x = the non trivial Element of F;

per cases ( not o in [#] F or ex a being Element of F st a = rpoly (n,(0. F)) ) ;

suppose A1: not o in [#] F ; :: thesis: ex K being non polynomial_disjoint Field ex p being Polynomial of K st
( K,F are_isomorphic & deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )

then reconsider K = ExField ( the non trivial Element of F,(rpoly (n,(0. F)))) as Field by Th7, Th8, Th10, Th9, Th12, Th11;
set p = rpoly (n,(0. K));

now :: thesis: for i being Element of NAT holds (rpoly (n,(0. F))) . i = (rpoly (n,(0. K))) . i

let i be Element of NAT ; :: thesis: (rpoly (n,(0. F))) . b₁ = (rpoly (n,(0. K))) . b₁

per cases ( i = 0 or i = n or ( i <> 0 & i <> n ) ) ;

suppose A2: i = 0 ; :: thesis: (rpoly (n,(0. F))) . b₁ = (rpoly (n,(0. K))) . b₁

hence (rpoly (n,(0. F))) . i = - ((power F) . ((0. F),n)) by HURWITZ:25
.= - (0. F) by Th6
.= - (0. K) by Def8
.= - ((power K) . ((0. K),n)) by Th6
.= (rpoly (n,(0. K))) . i by A2, HURWITZ:25 ;
:: thesis: verum

end;

suppose A3: i = n ; :: thesis: (rpoly (n,(0. F))) . b₁ = (rpoly (n,(0. K))) . b₁

hence (rpoly (n,(0. F))) . i = 1_ F by HURWITZ:25
.= 1_ K by Def8
.= (rpoly (n,(0. K))) . i by A3, HURWITZ:25 ;
:: thesis: verum

end;

suppose A4: ( i <> 0 & i <> n ) ; :: thesis: (rpoly (n,(0. F))) . b₁ = (rpoly (n,(0. K))) . b₁

hence (rpoly (n,(0. F))) . i = 0. F by HURWITZ:26
.= 0. K by Def8
.= (rpoly (n,(0. K))) . i by A4, HURWITZ:26 ;
:: thesis: verum

end;

end;

end;

then A5: rpoly (n,(0. F)) = rpoly (n,(0. K)) ;
A6: rpoly (n,(0. K)) in [#] (Polynom-Ring K) by POLYNOM3:def 10;
rpoly (n,(0. K)) in {(rpoly (n,(0. F)))} by A5, TARSKI:def 1;
then rpoly (n,(0. K)) in carr ( the non trivial Element of F,(rpoly (n,(0. F)))) by XBOOLE_0:def 3;
then A7: rpoly (n,(0. K)) in [#] K by Def8;
then rpoly (n,(0. K)) in ([#] K) /\ ([#] (Polynom-Ring K)) by A6, XBOOLE_0:def 4;
then reconsider K = K as non polynomial_disjoint Field by Def3;
take K ; :: thesis: ex p being Polynomial of K st
( K,F are_isomorphic & deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )
take p = rpoly (n,(0. K)); :: thesis: ( K,F are_isomorphic & deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )
( isoR ( the non trivial Element of F,(rpoly (n,(0. F)))) is additive & isoR ( the non trivial Element of F,(rpoly (n,(0. F)))) is multiplicative & isoR ( the non trivial Element of F,(rpoly (n,(0. F)))) is unity-preserving ) by A1, Th15;
hence K,F are_isomorphic by MOD_4:def 12, QUOFIELD:def 23; :: thesis: ( deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )
thus ( deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) ) by A7, A6, XBOOLE_0:def 4, HURWITZ:27; :: thesis: verum

end;

suppose A8: ex a being Element of F st a = rpoly (n,(0. F)) ; :: thesis: ex K being non polynomial_disjoint Field ex p being Polynomial of K st
( K,F are_isomorphic & deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )

then consider a being Element of F such that
A9: a = rpoly (n,(0. F)) ;
a in the carrier of (Polynom-Ring F) by A9, POLYNOM3:def 10;
then a in ([#] F) /\ ([#] (Polynom-Ring F)) by XBOOLE_0:def 4;
then reconsider K = F as non polynomial_disjoint Field by Def3;
take K ; :: thesis: ex p being Polynomial of K st
( K,F are_isomorphic & deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )
take x = rpoly (n,(0. K)); :: thesis: ( K,F are_isomorphic & deg x = n & x in ([#] K) /\ ([#] (Polynom-Ring K)) )
x in the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
hence ( K,F are_isomorphic & deg x = n & x in ([#] K) /\ ([#] (Polynom-Ring K)) ) by A8, HURWITZ:27, XBOOLE_0:def 4; :: thesis: verum

end;

end;