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