set f = rpoly (1,(0. F_Complex));
set p = [(rpoly (1,(0. F_Complex))),(1_. F_Complex)];

A1: now :: thesis: for x being Element of F_Complex holds eval ((rpoly (1,(0. F_Complex))),x) = x

let x be Element of F_Complex; :: thesis: eval ((rpoly (1,(0. F_Complex))),x) = x
thus eval ((rpoly (1,(0. F_Complex))),x) = x - (0. F_Complex) by HURWITZ:29
.= x by RLVECT_1:13 ; :: thesis: verum

end;

take [(rpoly (1,(0. F_Complex))),(1_. F_Complex)] ; :: thesis: ( not [(rpoly (1,(0. F_Complex))),(1_. F_Complex)] is zero & [(rpoly (1,(0. F_Complex))),(1_. F_Complex)] is odd & [(rpoly (1,(0. F_Complex))),(1_. F_Complex)] is real & [(rpoly (1,(0. F_Complex))),(1_. F_Complex)] is positive )
thus not [(rpoly (1,(0. F_Complex))),(1_. F_Complex)] is zero ; :: thesis: ( [(rpoly (1,(0. F_Complex))),(1_. F_Complex)] is odd & [(rpoly (1,(0. F_Complex))),(1_. F_Complex)] is real & [(rpoly (1,(0. F_Complex))),(1_. F_Complex)] is positive )
set fp = Polynomial-Function (F_Complex,(rpoly (1,(0. F_Complex))));

now :: thesis: for x being Element of F_Complex holds (Polynomial-Function (F_Complex,(rpoly (1,(0. F_Complex))))) . (- x) = - ((Polynomial-Function (F_Complex,(rpoly (1,(0. F_Complex))))) . x)

let x be Element of F_Complex; :: thesis: (Polynomial-Function (F_Complex,(rpoly (1,(0. F_Complex))))) . (- x) = - ((Polynomial-Function (F_Complex,(rpoly (1,(0. F_Complex))))) . x)
thus (Polynomial-Function (F_Complex,(rpoly (1,(0. F_Complex))))) . (- x) = eval ((rpoly (1,(0. F_Complex))),(- x)) by POLYNOM5:def 13
.= (- x) - (0. F_Complex) by HURWITZ:29
.= - x by RLVECT_1:13
.= - (x - (0. F_Complex)) by RLVECT_1:13
.= - (eval ((rpoly (1,(0. F_Complex))),x)) by HURWITZ:29
.= - ((Polynomial-Function (F_Complex,(rpoly (1,(0. F_Complex))))) . x) by POLYNOM5:def 13 ; :: thesis: verum

end;

then Polynomial-Function (F_Complex,(rpoly (1,(0. F_Complex)))) is odd ;
then rpoly (1,(0. F_Complex)) is odd ;
hence [(rpoly (1,(0. F_Complex))),(1_. F_Complex)] is odd ; :: thesis: ( [(rpoly (1,(0. F_Complex))),(1_. F_Complex)] is real & [(rpoly (1,(0. F_Complex))),(1_. F_Complex)] is positive )
reconsider z = 0 as Element of NAT by ORDINAL1:def 12;

now :: thesis: for i being Nat holds
( ([(rpoly (1,(0. F_Complex))),(1_. F_Complex)] `1) . i is Real & ([(rpoly (1,(0. F_Complex))),(1_. F_Complex)] `2) . i is Real )

let i be Nat; :: thesis: ( ([(rpoly (1,(0. F_Complex))),(1_. F_Complex)] `1) . i is Real & ([(rpoly (1,(0. F_Complex))),(1_. F_Complex)] `2) . i is Real )
A2: i in NAT by ORDINAL1:def 12;

now :: thesis: ( ( i = 0 & (rpoly (1,(0. F_Complex))) . i is Real ) or ( i = 1 & (rpoly (1,(0. F_Complex))) . i is Real ) or ( i <> 1 & i <> 0 & (rpoly (1,(0. F_Complex))) . i is Real ) )

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

case A3: i = 0 ; :: thesis: (rpoly (1,(0. F_Complex))) . i is Real

A4: 0 + 1 = 1 ;
(rpoly (1,(0. F_Complex))) . i = - ((power F_Complex) . ((0. F_Complex),1)) by A3, HURWITZ:25
.= - (((power F_Complex) . ((0. F_Complex),z)) * (0. F_Complex)) by A4, GROUP_1:def 7
.= 0. F_Complex by RLVECT_1:12 ;
hence (rpoly (1,(0. F_Complex))) . i is Real by COMPLFLD:def 1; :: thesis: verum

end;

case i = 1 ; :: thesis: (rpoly (1,(0. F_Complex))) . i is Real

then (rpoly (1,(0. F_Complex))) . i = 1. F_Complex by HURWITZ:25
.= 1r by COMPLFLD:def 1 ;
hence (rpoly (1,(0. F_Complex))) . i is Real by COMPLEX1:def 4; :: thesis: verum

end;

case ( i <> 1 & i <> 0 ) ; :: thesis: (rpoly (1,(0. F_Complex))) . i is Real

then (rpoly (1,(0. F_Complex))) . i = 0. F_Complex by HURWITZ:26, A2
.= 0 by COMPLFLD:def 1 ;
hence (rpoly (1,(0. F_Complex))) . i is Real ; :: thesis: verum

end;

end;

end;

hence ([(rpoly (1,(0. F_Complex))),(1_. F_Complex)] `1) . i is Real ; :: thesis: ([(rpoly (1,(0. F_Complex))),(1_. F_Complex)] `2) . i is Real
thus ([(rpoly (1,(0. F_Complex))),(1_. F_Complex)] `2) . i is Real ; :: thesis: verum

end;

hence [(rpoly (1,(0. F_Complex))),(1_. F_Complex)] is real ; :: thesis: [(rpoly (1,(0. F_Complex))),(1_. F_Complex)] is positive

now :: thesis: for x being Element of F_Complex st Re x > 0 & eval (([(rpoly (1,(0. F_Complex))),(1_. F_Complex)] `2),x) <> 0 holds
Re (eval ([(rpoly (1,(0. F_Complex))),(1_. F_Complex)],x)) > 0

let x be Element of F_Complex; :: thesis: ( Re x > 0 & eval (([(rpoly (1,(0. F_Complex))),(1_. F_Complex)] `2),x) <> 0 implies Re (eval ([(rpoly (1,(0. F_Complex))),(1_. F_Complex)],x)) > 0 )
assume A5: ( Re x > 0 & eval (([(rpoly (1,(0. F_Complex))),(1_. F_Complex)] `2),x) <> 0 ) ; :: thesis: Re (eval ([(rpoly (1,(0. F_Complex))),(1_. F_Complex)],x)) > 0
A6: eval ((1_. F_Complex),x) = 1_ F_Complex by POLYNOM4:18;
1. F_Complex <> 0. F_Complex ;
then A7: ((1. F_Complex) ") * (1. F_Complex) = 1. F_Complex by VECTSP_1:def 10;
eval ([(rpoly (1,(0. F_Complex))),(1_. F_Complex)],x) = x * ((1. F_Complex) ") by A1, A6
.= x * (1. F_Complex) by A7
.= x ;
hence Re (eval ([(rpoly (1,(0. F_Complex))),(1_. F_Complex)],x)) > 0 by A5; :: thesis: verum

end;

hence [(rpoly (1,(0. F_Complex))),(1_. F_Complex)] is positive ; :: thesis: verum