deffunc H₁( Point of [:(TOP-REAL 2),(TOP-REAL 2):]) -> Element of REAL = ($1 `2) `1 ;
consider xo being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A7: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds xo . x = H₁(x) from FUNCT_2:sch 4();
take xo ; :: thesis: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds xo . x = (x `2) `1
thus for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds xo . x = (x `2) `1 by A7; :: thesis: verum