set L = F_Complex ;
set x = 1. F_Complex;
set p = (() +* (0,())) +* (1,());
A1: dom () = NAT by FUNCOP_1:13;
then A2: dom (() +* (0,())) = NAT by FUNCT_7:30;
reconsider z = 0 as Element of NAT by ORDINAL1:def 12;
A3: ((() +* (0,())) +* (1,())) . 0 = (() +* (z,())) . z by FUNCT_7:32
.= 1. F_Complex by
.= 1 by ;
A4: ((() +* (0,())) +* (1,())) . 1 = 1. F_Complex by
.= 1 by ;
A5: now :: thesis: for i being Nat holds ((() +* (0,())) +* (1,())) . i is Real
let i be Nat; :: thesis: ((() +* (0,())) +* (1,())) . i is Real
now :: thesis: ( ( i = 0 & ((() +* (0,())) +* (1,())) . i is Real ) or ( i = 1 & ((() +* (0,())) +* (1,())) . i is Real ) or ( i >= 2 & ((() +* (0,())) +* (1,())) . i is Real ) )
per cases ( i = 0 or i = 1 or i >= 2 ) by NAT_1:23;
case i = 0 ; :: thesis: ((() +* (0,())) +* (1,())) . i is Real
hence (((0_. F_Complex) +* (0,())) +* (1,())) . i is Real by A3; :: thesis: verum
end;
case i = 1 ; :: thesis: ((() +* (0,())) +* (1,())) . i is Real
hence (((0_. F_Complex) +* (0,())) +* (1,())) . i is Real by A4; :: thesis: verum
end;
case A6: i >= 2 ; :: thesis: ((() +* (0,())) +* (1,())) . i is Real
then i <> 1 ;
then ((() +* (0,())) +* (1,())) . i = (() +* (0,())) . i by FUNCT_7:32
.= () . i by
.= 0. F_Complex by
.= 0 by COMPLFLD:def 1 ;
hence (((0_. F_Complex) +* (0,())) +* (1,())) . i is Real ; :: thesis: verum
end;
end;
end;
hence (((0_. F_Complex) +* (0,())) +* (1,())) . i is Real ; :: thesis: verum
end;
ex n being Nat st
for i being Nat st i >= n holds
((() +* (0,())) +* (1,())) . i = 0. F_Complex
proof
take 2 ; :: thesis: for i being Nat st i >= 2 holds
((() +* (0,())) +* (1,())) . i = 0. F_Complex

now :: thesis: for i being Nat st i >= 2 holds
((() +* (0,())) +* (1,())) . i = 0. F_Complex
let i be Nat; :: thesis: ( i >= 2 implies ((() +* (0,())) +* (1,())) . i = 0. F_Complex )
assume A7: i >= 2 ; :: thesis: ((() +* (0,())) +* (1,())) . i = 0. F_Complex
then 1 <> i ;
hence ((() +* (0,())) +* (1,())) . i = (() +* (0,())) . i by FUNCT_7:32
.= () . i by
.= 0. F_Complex by ;
:: thesis: verum
end;
hence for i being Nat st i >= 2 holds
((() +* (0,())) +* (1,())) . i = 0. F_Complex ; :: thesis: verum
end;
then reconsider p = (() +* (0,())) +* (1,()) 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:
then 1 <> i ;
hence p . i = (() +* (0,())) . i by FUNCT_7:32
.= () . i by
.= 0. F_Complex by ;
:: 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 < 2end;
hence 2 <= m ; :: thesis: verum
end;
then A11: len p = 2 by ;
reconsider p = p as real Polynomial of F_Complex by ;
take p ; :: thesis: ( not p is constant & p is with_positive_coefficients )
thus not p is constant by A11; :: thesis:
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 ;
now :: thesis: ( ( i = 0 & p . i > 0 ) or ( i = 1 & p . i > 0 ) )
per cases ( i = 0 or i = 1 ) by ;
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