let p be Polynomial of F_Complex; :: thesis: ( p is real implies p is real-valued )
assume A1: p is real ; :: thesis: p is real-valued

now :: thesis: for y being object st y in rng p holds
y in REAL

let y be object ; :: thesis: ( y in rng p implies y in REAL )
assume y in rng p ; :: thesis: y in REAL
then consider x being object such that
A2: ( x in dom p & p . x = y ) by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A2, FUNCT_2:def 1;
p . x is Real by A1;
hence y in REAL by A2, XREAL_0:def 1; :: thesis: verum

end;

hence p is real-valued by VALUED_0:def 3, TARSKI:def 3; :: thesis: verum