set L = F_Complex ;
set x = 1. F_Complex;
set p = ((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex));
A1: dom (0_. F_Complex) = NAT by FUNCOP_1:13;
then A2: dom ((0_. F_Complex) +* (0,(1. F_Complex))) = NAT by FUNCT_7:30;
reconsider z = 0 as Element of NAT by ORDINAL1:def 12;
A3: (((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . 0 = ((0_. F_Complex) +* (z,(1. F_Complex))) . z by FUNCT_7:32
.= 1. F_Complex by A1, FUNCT_7:31
.= 1 by COMPLFLD:def 1, COMPLEX1:def 4 ;
A4: (((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . 1 = 1. F_Complex by A2, FUNCT_7:31
.= 1 by COMPLFLD:def 1, COMPLEX1:def 4 ;

A5: now :: thesis: for i being Nat holds (((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i is Real

let i be Nat; :: thesis: (((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i is Real

now :: thesis: ( ( i = 0 & (((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i is Real ) or ( i = 1 & (((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i is Real ) or ( i >= 2 & (((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i is Real ) )

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

case i = 0 ; :: thesis: (((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i is Real

hence (((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i is Real by A3; :: thesis: verum

end;

case i = 1 ; :: thesis: (((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i is Real

hence (((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i is Real by A4; :: thesis: verum

end;

case A6: i >= 2 ; :: thesis: (((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i is Real

then i <> 1 ;
then (((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i = ((0_. F_Complex) +* (0,(1. F_Complex))) . i by FUNCT_7:32
.= (0_. F_Complex) . i by A6, FUNCT_7:32
.= 0. F_Complex by FUNCOP_1:7, ORDINAL1:def 12
.= 0 by COMPLFLD:def 1 ;
hence (((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i is Real ; :: thesis: verum

end;

end;

end;

hence (((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i is Real ; :: thesis: verum

end;

ex n being Nat st
for i being Nat st i >= n holds
(((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i = 0. F_Complex

proof

take 2 ; :: thesis: for i being Nat st i >= 2 holds
(((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i = 0. F_Complex

now :: thesis: for i being Nat st i >= 2 holds
(((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i = 0. F_Complex

let i be Nat; :: thesis: ( i >= 2 implies (((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i = 0. F_Complex )
assume A7: i >= 2 ; :: thesis: (((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i = 0. F_Complex
then 1 <> i ;
hence (((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i = ((0_. F_Complex) +* (0,(1. F_Complex))) . i by FUNCT_7:32
.= (0_. F_Complex) . i by A7, FUNCT_7:32
.= 0. F_Complex by ORDINAL1:def 12, FUNCOP_1:7 ;
:: thesis: verum

end;

hence for i being Nat st i >= 2 holds
(((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex))) . i = 0. F_Complex ; :: thesis: verum

end;

then reconsider p = ((0_. F_Complex) +* (0,(1. F_Complex))) +* (1,(1. F_Complex)) as Polynomial of F_Complex by ALGSEQ_1:def 1;

now :: thesis: for i being Nat st i >= 2 holds
p . i = 0. F_Complex

let i be Nat; :: thesis: ( i >= 2 implies p . i = 0. F_Complex )
assume A8: i >= 2 ; :: thesis: p . i = 0. F_Complex
then 1 <> i ;
hence p . i = ((0_. F_Complex) +* (0,(1. F_Complex))) . i by FUNCT_7:32
.= (0_. F_Complex) . i by A8, FUNCT_7:32
.= 0. F_Complex by ORDINAL1:def 12, FUNCOP_1:7 ;
:: thesis: verum

end;

then A9: 2 is_at_least_length_of p ;

now :: thesis: for m being Nat st m is_at_least_length_of p holds
2 <= m

let m be Nat; :: thesis: ( m is_at_least_length_of p implies 2 <= m )
assume A10: m is_at_least_length_of p ; :: thesis: 2 <= m

now :: thesis: not m < 2

assume m < 2 ; :: thesis: contradiction
then m < 1 + 1 ;
then p . 1 = 0. F_Complex by A10, INT_1:7;
hence contradiction by A2, FUNCT_7:31; :: thesis: verum

end;

hence 2 <= m ; :: thesis: verum

end;

then A11: len p = 2 by A9, ALGSEQ_1:def 3;
reconsider p = p as real Polynomial of F_Complex by A5, Def8;
take p ; :: thesis: ( not p is constant & p is with_positive_coefficients )
thus not p is constant by A11; :: thesis: p is with_positive_coefficients

now :: thesis: for i being Nat st i <= deg p holds
p . i > 0

let i be Nat; :: thesis: ( i <= deg p implies p . i > 0 )
assume i <= deg p ; :: thesis: p . i > 0
then A12: i < 1 + 1 by A11, NAT_1:13;

now :: thesis: ( ( i = 0 & p . i > 0 ) or ( i = 1 & p . i > 0 ) )

per cases ( i = 0 or i = 1 ) by A12, NAT_1:23;

case i = 0 ; :: thesis: p . i > 0

hence p . i > 0 by A3; :: thesis: verum

end;

case i = 1 ; :: thesis: p . i > 0

hence p . i > 0 by A4; :: thesis: verum

end;

end;

end;

hence p . i > 0 ; :: thesis: verum

end;

hence p is with_positive_coefficients ; :: thesis: verum