set F = the non almost_trivial Field;
set y = the non trivial Element of the non almost_trivial Field;
reconsider o = <%(0. the non almost_trivial Field),(1. 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 = <%(0. the non almost_trivial Field),(1. the non almost_trivial Field)%> ) ;

suppose not o in [#] the non almost_trivial Field ; :: thesis: ex K being Field ex x being object st
( not x in rng (canHom K) & x 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;
take K ; :: thesis: ex x being object st
( not x in rng (canHom K) & x in ([#] K) /\ ([#] (Polynom-Ring K)) )
take x = <%(0. K),(1. K)%>; :: thesis: ( not x in rng (canHom K) & x in ([#] K) /\ ([#] (Polynom-Ring K)) )

now :: thesis: for n being Element of NAT holds <%(0. the non almost_trivial Field),(1. the non almost_trivial Field)%> . n = <%(0. K),(1. K)%> . n

let n be Element of NAT ; :: thesis: <%(0. the non almost_trivial Field),(1. the non almost_trivial Field)%> . b₁ = <%(0. K),(1. K)%> . b₁

per cases ( n = 0 or n = 1 or n >= 2 ) by NAT_1:23;

suppose A1: n = 0 ; :: thesis: <%(0. the non almost_trivial Field),(1. the non almost_trivial Field)%> . b₁ = <%(0. K),(1. K)%> . b₁

hence <%(0. the non almost_trivial Field),(1. the non almost_trivial Field)%> . n = 0. the non almost_trivial Field by POLYNOM5:38
.= 0. K by Def8
.= <%(0. K),(1. K)%> . n by A1, POLYNOM5:38 ;
:: thesis: verum

end;

suppose A2: n = 1 ; :: thesis: <%(0. the non almost_trivial Field),(1. the non almost_trivial Field)%> . b₁ = <%(0. K),(1. K)%> . b₁

hence <%(0. the non almost_trivial Field),(1. the non almost_trivial Field)%> . n = 1. the non almost_trivial Field by POLYNOM5:38
.= 1. K by Def8
.= <%(0. K),(1. K)%> . n by A2, POLYNOM5:38 ;
:: thesis: verum

end;

suppose A3: n >= 2 ; :: thesis: <%(0. the non almost_trivial Field),(1. the non almost_trivial Field)%> . b₁ = <%(0. K),(1. K)%> . b₁

hence <%(0. the non almost_trivial Field),(1. the non almost_trivial Field)%> . n = 0. the non almost_trivial Field by POLYNOM5:38
.= 0. K by Def8
.= <%(0. K),(1. K)%> . n by A3, POLYNOM5:38 ;
:: thesis: verum

end;

end;

end;

then A4: <%(0. the non almost_trivial Field),(1. the non almost_trivial Field)%> = <%(0. K),(1. K)%> ;
then x in ([#] K) /\ ([#] (Polynom-Ring K)) by Th13;
then reconsider x = x as Element of the carrier of (Polynom-Ring K) ;
A5: deg x = (len x) - 1 by HURWITZ:def 2
.= 2 - 1 by POLYNOM5:40 ;

now :: thesis: not x in rng (canHom K)

assume x in rng (canHom K) ; :: thesis: contradiction
then consider a being object such that
A6: ( a in dom (canHom K) & x = (canHom K) . a ) by FUNCT_1:def 3;
reconsider a = a as Element of [#] K by A6;
deg (a | K) <= 0 by RATFUNC1:def 2;
hence contradiction by A6, A5, RING_4:def 6; :: thesis: verum

end;

hence ( not x in rng (canHom K) & x in ([#] K) /\ ([#] (Polynom-Ring K)) ) by A4, Th13; :: thesis: verum

end;

suppose A7: ex a being Element of the non almost_trivial Field st a = <%(0. the non almost_trivial Field),(1. the non almost_trivial Field)%> ; :: thesis: ex K being Field ex x being object st
( not x in rng (canHom K) & x in ([#] K) /\ ([#] (Polynom-Ring K)) )

take the non almost_trivial Field ; :: thesis: ex x being object st
( not x in rng (canHom the non almost_trivial Field) & x in ([#] the non almost_trivial Field) /\ ([#] (Polynom-Ring the non almost_trivial Field)) )
take x = <%(0. the non almost_trivial Field),(1. the non almost_trivial Field)%>; :: thesis: ( not x in rng (canHom the non almost_trivial Field) & x in ([#] the non almost_trivial Field) /\ ([#] (Polynom-Ring the non almost_trivial Field)) )
2 = len x by POLYNOM5:40;
then A8: deg x = 2 - 1 by HURWITZ:def 2;
A9: x in the carrier of (Polynom-Ring the non almost_trivial Field) by POLYNOM3:def 10;

now :: thesis: not x in rng (canHom the non almost_trivial Field)

assume x in rng (canHom the non almost_trivial Field) ; :: thesis: contradiction
then consider a being object such that
A10: ( a in dom (canHom the non almost_trivial Field) & x = (canHom the non almost_trivial Field) . a ) by FUNCT_1:def 3;
reconsider a = a as Element of [#] the non almost_trivial Field by A10;
deg (a | the non almost_trivial Field) <= 0 by RATFUNC1:def 2;
hence contradiction by A10, A8, RING_4:def 6; :: thesis: verum

end;

hence ( not x in rng (canHom the non almost_trivial Field) & x in ([#] the non almost_trivial Field) /\ ([#] (Polynom-Ring the non almost_trivial Field)) ) by A7, A9, XBOOLE_0:def 4; :: thesis: verum

end;

end;