Eval (0_. F_Real) = REAL --> (In (0,REAL))

proof

let r be Element of REAL ; :: according to FUNCT_2:def 8 :: thesis: (Eval (0_. F_Real)) . r = (REAL --> (In (0,REAL))) . r
thus (Eval (0_. F_Real)) . r = eval ((0_. F_Real),(In (r,F_Real))) by POLYNOM5:def 13
.= In (0,REAL) by POLYNOM4:17
.= (REAL --> (In (0,REAL))) . r ; :: thesis: verum

end;

hence Eval (0_. F_Real) = REAL --> 0 ; :: thesis: verum