deffunc H₁( Element of REAL ) -> Element of REAL = $1 ^2 ;
consider G being Function of REAL,REAL such that
A1: for x being Element of REAL holds G . x = H₁(x) from FUNCT_2:sch 4();
take G ; :: thesis: for r being real number holds G . r = r ^2
let r be real number ; :: thesis: G . r = r ^2
r in REAL by XREAL_0:def 1;
hence G . r = r ^2 by A1; :: thesis: verum