set p = 1_. F_Complex;

thus 1_. F_Complex is positive by POLYNOM4:18, COMPLFLD:8, COMPLEX1:6; :: thesis: verum

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

hence
1_. F_Complex is real
; :: thesis: 1_. F_Complex is positive let i be Nat; :: thesis: (1_. F_Complex) . i is Real

end;now :: thesis: ( ( i = 0 & (1_. F_Complex) . i is Real ) or ( i <> 0 & (1_. F_Complex) . i is Real ) )

hence
(1_. F_Complex) . i is Real
; :: thesis: verumend;

thus 1_. F_Complex is positive by POLYNOM4:18, COMPLFLD:8, COMPLEX1:6; :: thesis: verum