deffunc H₁( Element of Morphs V) -> strict Element of V = cod $1;
consider F being Function of (Morphs V),V such that
A4: 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 = cod f
thus for f being Element of Morphs V holds F . f = cod f by A4; :: thesis: verum