deffunc H1( Element of COMPLEX ) -> Element of REAL = In (|.$1.|,REAL);
consider F being Function of COMPLEX,REAL such that
A1:
for c being Element of COMPLEX holds F . c = H1(c)
from FUNCT_2:sch 4();
take
F
; for c being Element of COMPLEX holds F . c = |.c.|
let c be Element of COMPLEX ; F . c = |.c.|
thus F . c =
H1(c)
by A1
.=
|.c.|
; verum