let V be set ; for C being finite set
for A being Element of SubstitutionSet (V,C) st A = {} holds
- A = {{}}
let C be finite set ; for A being Element of SubstitutionSet (V,C) st A = {} holds
- A = {{}}
let A be Element of SubstitutionSet (V,C); ( A = {} implies - A = {{}} )
defpred S1[ 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 = {}
; - 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) : S1[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; verum