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 = {} )
assume A1:
A = {{}}
; - A = {}
assume
- A <> {}
; contradiction
then consider x1 being object such that
A2:
x1 in - A
by XBOOLE_0:def 1;
consider f1 being Element of PFuncs ((Involved A),C) such that
x1 = f1
and
A3:
for g being Element of PFuncs (V,C) st g in {{}} holds
not f1 tolerates g
by A1, A2;
A4:
{} in {{}}
by TARSKI:def 1;
{} is PartFunc of V,C
by RELSET_1:12;
then A5:
{} in PFuncs (V,C)
by PARTFUN1:45;
f1 tolerates {}
by PARTFUN1:59;
hence
contradiction
by A3, A5, A4; verum