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) /\ ([#] ()) )

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) /\ ([#] ()) )

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) /\ ([#] ()) )

then reconsider K = ExField ( the non trivial Element of F,(rpoly (n,(0. F)))) as Field by ;
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))) . b1 = (rpoly (n,(0. K))) . b1
per cases ( i = 0 or i = n or ( i <> 0 & i <> n ) ) ;
suppose A2: i = 0 ; :: thesis: (rpoly (n,(0. F))) . b1 = (rpoly (n,(0. K))) . b1
hence (rpoly (n,(0. F))) . i = - (() . ((0. F),n)) by HURWITZ:25
.= - (0. F) by Th6
.= - (0. K) by Def8
.= - (() . ((0. K),n)) by Th6
.= (rpoly (n,(0. K))) . i by ;
:: thesis: verum
end;
suppose A3: i = n ; :: thesis: (rpoly (n,(0. F))) . b1 = (rpoly (n,(0. K))) . b1
hence (rpoly (n,(0. F))) . i = 1_ F by HURWITZ:25
.= 1_ K by Def8
.= (rpoly (n,(0. K))) . i by ;
:: thesis: verum
end;
suppose A4: ( i <> 0 & i <> n ) ; :: thesis: (rpoly (n,(0. F))) . b1 = (rpoly (n,(0. K))) . b1
hence (rpoly (n,(0. F))) . i = 0. F by HURWITZ:26
.= 0. K by Def8
.= (rpoly (n,(0. K))) . i by ;
:: thesis: verum
end;
end;
end;
then A5: rpoly (n,(0. F)) = rpoly (n,(0. K)) ;
A6: rpoly (n,(0. K)) in [#] () by POLYNOM3:def 10;
rpoly (n,(0. K)) in {(rpoly (n,(0. F)))} by ;
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) /\ ([#] ()) by ;
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) /\ ([#] ()) )

take p = rpoly (n,(0. K)); :: thesis: ( K,F are_isomorphic & deg p = n & p in ([#] 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 ;
hence K,F are_isomorphic by ; :: thesis: ( deg p = n & p in ([#] K) /\ ([#] ()) )
thus ( deg p = n & p in ([#] K) /\ ([#] ()) ) by ; :: 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) /\ ([#] ()) )

then consider a being Element of F such that
A9: a = rpoly (n,(0. F)) ;
a in the carrier of () by ;
then a in ([#] 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) /\ ([#] ()) )

take x = rpoly (n,(0. K)); :: thesis: ( K,F are_isomorphic & deg x = n & x in ([#] K) /\ ([#] ()) )
x in the carrier of () by POLYNOM3:def 10;
hence ( K,F are_isomorphic & deg x = n & x in ([#] K) /\ ([#] ()) ) by ; :: thesis: verum
end;
end;