for r being Element of F_Real holds Eval <%r%> = REAL --> r