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