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 = {} )
assume A1: A = {{}} ; :: thesis: - A = {}
assume - A <> {} ; :: thesis: 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; :: thesis: verum