let V be set ; :: thesis: for C being finite set
for A being Element of SubstitutionSet (V,C) st A = {} holds
- A = {{}}
let C be finite set ; :: thesis: for A being Element of SubstitutionSet (V,C) st A = {} holds
- A = {{}}
let A be Element of SubstitutionSet (V,C); :: thesis: ( A = {} implies - A = {{}} )
defpred S₁[ Element of PFuncs ((Involved A),C)] means for g being Element of PFuncs (V,C) st g in A holds
not $1 tolerates g;
assume A1: A = {} ; :: thesis: - A = {{}}
then A2: for g being Element of PFuncs (V,C) st g in A holds
not {} tolerates g ;
{ xx where xx is Element of PFuncs ((Involved A),C) : S₁[xx] } c= PFuncs ((Involved A),C) from FRAENKEL:sch 10();
then - A c= PFuncs ({},C) by A1, Th7;
then A3: - A c= {{}} by PARTFUN1:48;
{} in {{}} by TARSKI:def 1;
then {} in PFuncs ({},C) by PARTFUN1:48;
then {} in PFuncs ((Involved A),C) by A1, Th7;
then {} in - A by A2;
then {{}} c= - A by ZFMISC_1:31;
hence - A = {{}} by A3; :: thesis: verum