deffunc H₁( Point of [:(TOP-REAL 2),(TOP-REAL 2):]) -> Element of REAL = (($1 `2 ) `1 ) - (o `1 );
consider xo being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A1: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds xo . x = H<sub>1</sub>(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 ) - (o `1 )
thus for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds xo . x = ((x `2 ) `1 ) - (o `1 ) by A1; :: thesis: verum