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

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

hence
p is real-valued
by VALUED_0:def 3, TARSKI:def 3; :: thesis: verumy 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;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