deffunc H₁( Element of Morphs V) -> Element of V = dom' $1;
consider F being Function of (Morphs V),V such that
A1: for f being Element of Morphs V holds F . f = H₁(f) from FUNCT_2:sch 4();
take F ; :: thesis: for f being Element of Morphs V holds F . f = dom' f
thus for f being Element of Morphs V holds F . f = dom' f by A1; :: thesis: verum