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