deffunc H₁( Point of (TOP-REAL 2)) -> Element of REAL = In (($1 `1),REAL);
consider f being RealMap of (TOP-REAL 2) such that
A1: for p being Point of (TOP-REAL 2) holds f . p = H<sub>1</sub>(p) from FUNCT_2:sch 4();
take f ; :: thesis: for p being Point of (TOP-REAL 2) holds f . p = p `1
let p be Point of (TOP-REAL 2); :: thesis: f . p = p `1
f . p = H<sub>1</sub>(p) by A1;
hence f . p = p `1 ; :: thesis: verum