let I be real Polynomial of F_Complex; :: thesis: for r being real Element of F_Complex holds eval (I,r) is real
let r be real Element of F_Complex; :: thesis: eval (I,r) is real
consider H being FinSequence of F_Complex such that
A1: ( eval (I,r) = Sum H & len H = len I ) and
A2: for n being Element of NAT st n in dom H holds
H . n = (I . (n -' 1)) * ((power F_Complex) . (r,(n -' 1))) by POLYNOM4:def 2;
consider h being sequence of the carrier of F_Complex such that
A3: Sum H = h . (len H) and
A4: ( h . 0 = 0. F_Complex & ( for j being Nat
for v being Element of F_Complex st j < len H & v = H . (j + 1) holds
h . (j + 1) = (h . j) + v ) ) by RLVECT_1:def 12;
defpred S₁[ Nat] means ( $1 <= len H implies h . $1 is real );
A5: S₁[ 0 ] by A4;
A6: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A7: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
assume A8: n + 1 <= len H ; :: thesis: h . (n + 1) is real
n + 1 in dom H by NAT_1:11, A8, FINSEQ_3:25;
then A9: H . (n + 1) = (I . ((n + 1) -' 1)) * ((power F_Complex) . (r,((n + 1) -' 1))) by A2;
reconsider Hn1 = H . (n + 1) as real Element of F_Complex by A9;
h . (n + 1) = (h . n) + Hn1 by A4, A8, NAT_1:13;
hence h . (n + 1) is real by A8, A7, NAT_1:13; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A6);
hence eval (I,r) is real by A1, A3; :: thesis: verum