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 5();
u in the carrier of (SubstLatt (V,C)) ;
then A14: u in SubstitutionSet (V,C) by SUBSTLAT:def 4;
for x being object st x in the carrier of (SubstLatt (V,C)) holds
IT . x in Fin (PFuncs (V,C))

proof

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

end;

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

now :: thesis: for v being Element of (SubstLatt (V,C)) holds IT . v in the carrier of (SubstLatt (V,C))

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