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 ;
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)) ) ;
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)) )
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));
now :: thesis: for i being Element of NAT holds (rpoly (n,(0. the non almost_trivial Field))) . i = (rpoly (n,(0. K))) . i
let i be Element of NAT ; :: thesis: (rpoly (n,(0. the non almost_trivial Field))) . b1 = (rpoly (n,(0. K))) . b1
per cases ( i = 0 or i = n or ( i <> 0 & i <> n ) ) ;
suppose A1: i = 0 ; :: thesis: (rpoly (n,(0. the non almost_trivial Field))) . b1 = (rpoly (n,(0. K))) . b1
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;
suppose A2: i = n ; :: thesis: (rpoly (n,(0. the non almost_trivial Field))) . b1 = (rpoly (n,(0. K))) . b1
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;
suppose A3: ( i <> 0 & i <> n ) ; :: thesis: (rpoly (n,(0. the non almost_trivial Field))) . b1 = (rpoly (n,(0. K))) . b1
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;
end;
end;
then A4: rpoly (n,(0. the non almost_trivial Field)) = 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;
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)) )
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;
end;