let r be Element of F_Real; :: thesis: Eval <%r%> = REAL --> r
Eval <%r%> = REAL --> (In (r,REAL))
proof
let a be Element of REAL ; :: according to FUNCT_2:def 8 :: thesis: (Eval <%r%>) . a = (REAL --> (In (r,REAL))) . a
thus (Eval <%r%>) . a = eval (<%r%>,(In (a,F_Real))) by POLYNOM5:def 13
.= r by POLYNOM5:37
.= (REAL --> (In (r,REAL))) . a ; :: thesis: verum
end;
hence Eval <%r%> = REAL --> r ; :: thesis: verum