deffunc H₁( set ) -> set = {} ;
let V be set ; :: thesis: for C being finite set
for A being Element of Fin (PFuncs (V,C)) st A = {} holds
A =>> A = {{}}
let C be finite set ; :: thesis: for A being Element of Fin (PFuncs (V,C)) st A = {} holds
A =>> A = {{}}
let A be Element of Fin (PFuncs (V,C)); :: thesis: ( A = {} implies A =>> A = {{}} )
defpred S₁[ Function] means dom $1 = A;
deffunc H₂( Element of PFuncs (A,A)) -> set = union { (($1 . i) \ i) where i is Element of PFuncs (V,C) : i in A } ;
A1: ex a being Element of PFuncs (A,A) st S₁[a]

proof

reconsider e = id A as Element of PFuncs (A,A) by PARTFUN1:45;
take e ; :: thesis: S₁[e]
thus S₁[e] ; :: thesis: verum

end;

A2: { {} where f is Element of PFuncs (A,A) : S₁[f] } = {{}} from LATTICE3:sch 1(A1);
assume A3: A = {} ; :: thesis: A =>> A = {{}}

now :: thesis: for f being Element of PFuncs (A,A) holds { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } = {}

let f be Element of PFuncs (A,A); :: thesis: { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } = {}
for x being object holds not x in { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A }

proof

given x being object such that A4: x in { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } ; :: thesis: contradiction
ex x1 being Element of PFuncs (V,C) st
( x = (f . x1) \ x1 & x1 in A ) by A4;
hence contradiction by A3; :: thesis: verum

end;

hence { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } = {} by XBOOLE_0:def 1; :: thesis: verum

end;

then A5: for v being Element of PFuncs (A,A) st S₁[v] holds
H₂(v) = H₁(v) by ZFMISC_1:2;
A6: { H₂(f) where f is Element of PFuncs (A,A) : S₁[f] } = { H₁(f) where f is Element of PFuncs (A,A) : S₁[f] } from FRAENKEL:sch 6(A5);
{} is PartFunc of V,C by RELSET_1:12;
then {} in PFuncs (V,C) by PARTFUN1:45;
then {{}} c= PFuncs (V,C) by ZFMISC_1:31;
hence A =>> A = {{}} by A6, A2, XBOOLE_1:28; :: thesis: verum