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;

( 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)) )
;

end;

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)) )

( 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));

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;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

then A5:
rpoly (n,(0. F)) = rpoly (n,(0. K))
;let i be Element of NAT ; :: thesis: (rpoly (n,(0. F))) . b_{1} = (rpoly (n,(0. K))) . b_{1}

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

end;

suppose A2:
i = 0
; :: thesis: (rpoly (n,(0. F))) . b_{1} = (rpoly (n,(0. K))) . b_{1}

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;.= - (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

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

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)) )

( 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;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