deffunc H1( 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 S1[ Function] means dom $1 = A;
deffunc H2( 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 S1[a]
proof
reconsider e = id A as Element of PFuncs (A,A) by PARTFUN1:45;
take e ; :: thesis: S1[e]
thus S1[e] ; :: thesis: verum
end;
A2: { {} where f is Element of PFuncs (A,A) : S1[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 S1[v] holds
H2(v) = H1(v) by ZFMISC_1:2;
A6: { H2(f) where f is Element of PFuncs (A,A) : S1[f] } = { H1(f) where f is Element of PFuncs (A,A) : S1[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