deffunc H₁( Element of X * ) -> Element of Y * = f * $1;
consider g being Function of (X *),(Y *) such that
A1: for x being Element of X * holds g . x = H₁(x) from FUNCT_2:sch 4();
take g ; :: thesis: for p being Element of X * holds g . p = f * p
thus for p being Element of X * holds g . p = f * p by A1; :: thesis: verum