set p = 0_. F_Complex;

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

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

hence
0_. F_Complex is real
; :: thesis: not 0_. F_Complex is positive 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;(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

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