A1: the carrier of (SubstLatt V,C) = SubstitutionSet V,C by SUBSTLAT:def 4;
deffunc H₁( Element of PFuncs V,C) -> Element of SubstitutionSet V,C = mi {.$1.};
consider f being Function of PFuncs V,C, SubstitutionSet V,C such that
A2: for a being Element of PFuncs V,C holds f . a = H₁(a) from FUNCT_2:sch 4();

A3: now

let x be set ; :: thesis: ( x in PFuncs V,C implies f . x in the carrier of (SubstLatt V,C) )
assume x in PFuncs V,C ; :: thesis: f . x in the carrier of (SubstLatt V,C)
then reconsider a = x as Element of PFuncs V,C ;
f . a = mi {.a.} by A2;
hence f . x in the carrier of (SubstLatt V,C) by A1; :: thesis: verum

end;

dom f = PFuncs V,C by FUNCT_2:def 1;
then reconsider f = f as Function of PFuncs V,C,the carrier of (SubstLatt V,C) by A3, FUNCT_2:5;
take f ; :: thesis: for a being Element of PFuncs V,C holds f . a = mi {.a.}
thus for a being Element of PFuncs V,C holds f . a = mi {.a.} by A2; :: thesis: verum