deffunc H₁( Real) -> Element of REAL = In (($1 ^2),REAL);
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 holds G . r = r ^2
let r be Real; :: thesis: G . r = r ^2
r in REAL by XREAL_0:def 1;
then G . r = H₁(r) by A1;
hence G . r = r ^2 ; :: thesis: verum