let n be non zero Nat; :: thesis: ex K being Field ex p being Polynomial of K st

( deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )

reconsider n = n as Element of NAT by ORDINAL1:def 12;

set F = the non almost_trivial Field;

set x = the non trivial Element of the non almost_trivial Field;

reconsider o = rpoly (n,(0. the non almost_trivial Field)) as object ;

( deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )

reconsider n = n as Element of NAT by ORDINAL1:def 12;

set F = the non almost_trivial Field;

set x = the non trivial Element of the non almost_trivial Field;

reconsider o = rpoly (n,(0. the non almost_trivial Field)) as object ;

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

end;

suppose
not o in [#] the non almost_trivial Field
; :: thesis: ex K being Field ex p being Polynomial of K st

( deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )

( deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )

then reconsider K = ExField ( the non trivial Element of the non almost_trivial Field,o) as Field by Th7, Th8, Th10, Th9, Th12, Th11;

set p = rpoly (n,(0. K));

take K ; :: thesis: ex p being Polynomial of K st

( deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )

take p = rpoly (n,(0. K)); :: thesis: ( deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )

A5: p in [#] (Polynom-Ring K) by POLYNOM3:def 10;

p in {(rpoly (n,(0. the non almost_trivial Field)))} by A4, TARSKI:def 1;

then p in carr ( the non trivial Element of the non almost_trivial Field,(rpoly (n,(0. the non almost_trivial Field)))) by XBOOLE_0:def 3;

then p in [#] K by Def8;

hence ( deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) ) by A5, 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. the non almost_trivial Field))) . i = (rpoly (n,(0. K))) . i

then A4:
rpoly (n,(0. the non almost_trivial Field)) = rpoly (n,(0. K))
;let i be Element of NAT ; :: thesis: (rpoly (n,(0. the non almost_trivial Field))) . b_{1} = (rpoly (n,(0. K))) . b_{1}

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

end;

suppose A1:
i = 0
; :: thesis: (rpoly (n,(0. the non almost_trivial Field))) . b_{1} = (rpoly (n,(0. K))) . b_{1}

hence (rpoly (n,(0. the non almost_trivial Field))) . i =
- ((power the non almost_trivial Field) . ((0. the non almost_trivial Field),n))
by HURWITZ:25

.= - (0. the non almost_trivial Field) by Th6

.= - (0. K) by Def8

.= - ((power K) . ((0. K),n)) by Th6

.= (rpoly (n,(0. K))) . i by A1, HURWITZ:25 ;

:: thesis: verum

end;.= - (0. the non almost_trivial Field) by Th6

.= - (0. K) by Def8

.= - ((power K) . ((0. K),n)) by Th6

.= (rpoly (n,(0. K))) . i by A1, HURWITZ:25 ;

:: thesis: verum

suppose A2:
i = n
; :: thesis: (rpoly (n,(0. the non almost_trivial Field))) . b_{1} = (rpoly (n,(0. K))) . b_{1}

hence (rpoly (n,(0. the non almost_trivial Field))) . i =
1_ the non almost_trivial Field
by HURWITZ:25

.= 1_ K by Def8

.= (rpoly (n,(0. K))) . i by A2, HURWITZ:25 ;

:: thesis: verum

end;.= 1_ K by Def8

.= (rpoly (n,(0. K))) . i by A2, HURWITZ:25 ;

:: thesis: verum

suppose A3:
( i <> 0 & i <> n )
; :: thesis: (rpoly (n,(0. the non almost_trivial Field))) . b_{1} = (rpoly (n,(0. K))) . b_{1}

hence (rpoly (n,(0. the non almost_trivial Field))) . i =
0. the non almost_trivial Field
by HURWITZ:26

.= 0. K by Def8

.= (rpoly (n,(0. K))) . i by A3, HURWITZ:26 ;

:: thesis: verum

end;.= 0. K by Def8

.= (rpoly (n,(0. K))) . i by A3, HURWITZ:26 ;

:: thesis: verum

take K ; :: thesis: ex p being Polynomial of K st

( deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )

take p = rpoly (n,(0. K)); :: thesis: ( deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )

A5: p in [#] (Polynom-Ring K) by POLYNOM3:def 10;

p in {(rpoly (n,(0. the non almost_trivial Field)))} by A4, TARSKI:def 1;

then p in carr ( the non trivial Element of the non almost_trivial Field,(rpoly (n,(0. the non almost_trivial Field)))) by XBOOLE_0:def 3;

then p in [#] K by Def8;

hence ( deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) ) by A5, XBOOLE_0:def 4, HURWITZ:27; :: thesis: verum

suppose A6:
ex a being Element of the non almost_trivial Field st a = rpoly (n,(0. the non almost_trivial Field))
; :: thesis: ex K being Field ex p being Polynomial of K st

( deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )

( deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )

take
the non almost_trivial Field
; :: thesis: ex p being Polynomial of the non almost_trivial Field st

( deg p = n & p in ([#] the non almost_trivial Field) /\ ([#] (Polynom-Ring the non almost_trivial Field)) )

take x = rpoly (n,(0. the non almost_trivial Field)); :: thesis: ( deg x = n & x in ([#] the non almost_trivial Field) /\ ([#] (Polynom-Ring the non almost_trivial Field)) )

x in [#] (Polynom-Ring the non almost_trivial Field) by POLYNOM3:def 10;

hence ( deg x = n & x in ([#] the non almost_trivial Field) /\ ([#] (Polynom-Ring the non almost_trivial Field)) ) by A6, HURWITZ:27, XBOOLE_0:def 4; :: thesis: verum

end;( deg p = n & p in ([#] the non almost_trivial Field) /\ ([#] (Polynom-Ring the non almost_trivial Field)) )

take x = rpoly (n,(0. the non almost_trivial Field)); :: thesis: ( deg x = n & x in ([#] the non almost_trivial Field) /\ ([#] (Polynom-Ring the non almost_trivial Field)) )

x in [#] (Polynom-Ring the non almost_trivial Field) by POLYNOM3:def 10;

hence ( deg x = n & x in ([#] the non almost_trivial Field) /\ ([#] (Polynom-Ring the non almost_trivial Field)) ) by A6, HURWITZ:27, XBOOLE_0:def 4; :: thesis: verum