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: for x being object st x in PFuncs (V,C) holds
f . x in the carrier of (SubstLatt (V,C))

let x be object ; :: 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 A1;
hence f . x in the carrier of (SubstLatt (V,C)) by A2; :: 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:3;
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 A1; :: thesis: verum