deffunc H₁( set ) -> Element of bool u = u \ $1;
consider IT being Function such that
A13: ( dom IT = the carrier of (SubstLatt V,C) & ( for v being set st v in the carrier of (SubstLatt V,C) holds
IT . v = H₁(v) ) ) from FUNCT_1:sch 3();
u in the carrier of (SubstLatt V,C) ;
then A14: u in SubstitutionSet V,C by SUBSTLAT:def 4;
for x being set st x in the carrier of (SubstLatt V,C) holds
IT . x in Fin (PFuncs V,C)

proof

let x be set ; :: thesis: ( x in the carrier of (SubstLatt V,C) implies IT . x in Fin (PFuncs V,C) )
assume x in the carrier of (SubstLatt V,C) ; :: thesis: IT . x in Fin (PFuncs V,C)
then A15: IT . x = u \ x by A13;
u \ x in SubstitutionSet V,C by A14, Lm4;
hence IT . x in Fin (PFuncs V,C) by A15; :: thesis: verum

end;

then reconsider IT = IT as Function of the carrier of (SubstLatt V,C),(Fin (PFuncs V,C)) by A13, FUNCT_2:5;

now

let v be Element of (SubstLatt V,C); :: thesis: IT . v in the carrier of (SubstLatt V,C)
u \ v in SubstitutionSet V,C by A14, Lm4;
then IT . v in SubstitutionSet V,C by A13;
hence IT . v in the carrier of (SubstLatt V,C) by SUBSTLAT:def 4; :: thesis: verum

end;

then reconsider IT = IT as UnOp of the carrier of (SubstLatt V,C) by HEYTING1:1;
take IT ; :: thesis: for v being Element of (SubstLatt V,C) holds IT . v = u \ v
let v be Element of (SubstLatt V,C); :: thesis: IT . v = u \ v
thus IT . v = u \ v by A13; :: thesis: verum