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:119;
take e ; :: thesis: S₁[e]
thus S₁[e] by RELAT_1:71; :: 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

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 set holds not x in { ((f . i) \ i) where i is Element of PFuncs V,C : i in A }

proof

given x being set 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:25;
then {} in PFuncs V,C by PARTFUN1:119;
then {{} } c= PFuncs V,C by ZFMISC_1:37;
hence A =>> A = {{} } by A6, A2, XBOOLE_1:28; :: thesis: verum