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 set 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:25;
then A5: {} in PFuncs V,C by PARTFUN1:119;
f1 tolerates {} by PARTFUN1:141;
hence contradiction by A3, A5, A4; :: thesis: verum