set p = 1_. F_Complex;

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

let i be Nat; :: thesis: (1_. F_Complex) . i is real number

now :: thesis: ( ( i = 0 & (1_. F_Complex) . i is real number ) or ( i <> 0 & (1_. F_Complex) . i is real number ) )

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

case i = 0 ; :: thesis: (1_. F_Complex) . i is real number

then (1_. F_Complex) . i = 1. F_Complex by POLYNOM3:30
.= 1 by COMPLEX1:def 4, COMPLFLD:def 1 ;
hence (1_. F_Complex) . i is real number ; :: thesis: verum

end;

case i <> 0 ; :: thesis: (1_. F_Complex) . i is real number

then (1_. F_Complex) . i = 0. F_Complex by POLYNOM3:30
.= 0 by COMPLFLD:def 1 ;
hence (1_. F_Complex) . i is real number ; :: thesis: verum

end;

end;

end;

hence (1_. F_Complex) . i is real number ; :: thesis: verum

end;

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