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