set p = 0_. F_Complex;

now :: thesis: for i being Nat holds (0_. F_Complex) . i is Real

let i be Nat; :: thesis: (0_. F_Complex) . i is Real
(0_. F_Complex) . i = 0. F_Complex by FUNCOP_1:7, ORDINAL1:def 12
.= 0 by COMPLFLD:def 1 ;
hence (0_. F_Complex) . i is Real ; :: thesis: verum

end;

hence 0_. F_Complex is real ; :: thesis: not 0_. F_Complex is positive
A1: Re (1. F_Complex) > 0 by COMPLEX1:6, COMPLFLD:def 1;
eval ((0_. F_Complex),(1. F_Complex)) = 0. F_Complex by POLYNOM4:17
.= 0 by COMPLFLD:def 1 ;
hence not 0_. F_Complex is positive by A1, COMPLEX1:4; :: thesis: verum