deffunc H₁( Point of (TOP-REAL 2)) -> Element of REAL = In (($1 `2),REAL);
consider f being RealMap of (TOP-REAL 2) such that
A4: 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 `2
let p be Point of (TOP-REAL 2); :: thesis: f . p = p `2
f . p = H<sub>1</sub>(p) by A4;
hence f . p = p `2 ; :: thesis: verum