deffunc H₂( Object of C) -> Morphism of $1,$1 = id $1;
consider f being Function of the carrier of C, the carrier' of C such that
A1: for o being Object of C holds f . o = H₂(o) from FUNCT_2:sch 4();
take f ; :: thesis: for o being Object of C holds f . o = id o
thus for o being Object of C holds f . o = id o by A1; :: thesis: verum