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
A1: for a being Element of PFuncs (V,C) holds f . a = H₁(a) from FUNCT_2:sch 4();
A2: the carrier of (SubstLatt (V,C)) = SubstitutionSet (V,C) by SUBSTLAT:def 4;

A3: now :: thesis:

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

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:3;
take f ; :: thesis:
thus for a being Element of PFuncs (V,C) holds f . a = mi {.a.} by A1; :: thesis: