deffunc H₁( set ) -> Element of REAL = Re (f /. $1);
thus for h, g being PartFunc of COMPLEX ,REAL st dom h = dom f & ( for z being Complex st z in dom h holds
h . z = H₁(z) ) & dom g = dom f & ( for z being Complex st z in dom g holds
g . z = H₁(z) ) holds
h = g from SEQ_1:sch 4(); :: thesis: verum