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 = {{} } )
assume A1: A = {} ; :: thesis: 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 } ;
deffunc H₂( set ) -> set = {} ;

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 A2: x in { ((f . i) \ i) where i is Element of PFuncs V,C : i in A } ; :: thesis: contradiction
consider x1 being Element of PFuncs V,C such that
A3: ( x = (f . x1) \ x1 & x1 in A ) by A2;
thus contradiction by A1, 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 A4: for v being Element of PFuncs A,A st S₁[v] holds
H₁(v) = H₂(v) by ZFMISC_1:2;
A5: { 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(A4);
A6: 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;

A7: { {} where f is Element of PFuncs A,A : S₁[f] } = {{} } from LATTICE3:sch 1(A6);
{} 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 A5, A7, XBOOLE_1:28; :: thesis: verum