let V be set ; :: thesis: for C being finite set
for K being Element of SubstitutionSet (V,C)
for X being set st X c= K holds
X in SubstitutionSet (V,C)
let C be finite set ; :: thesis: for K being Element of SubstitutionSet (V,C)
for X being set st X c= K holds
X in SubstitutionSet (V,C)
let K be Element of SubstitutionSet (V,C); :: thesis: for X being set st X c= K holds
X in SubstitutionSet (V,C)
let X be set ; :: thesis: ( X c= K implies X in SubstitutionSet (V,C) )
assume A1: X c= K ; :: thesis: X in SubstitutionSet (V,C)
K c= PFuncs (V,C) by FINSUB_1:def 5;
then X c= PFuncs (V,C) by A1;
then reconsider B = X as Element of Fin (PFuncs (V,C)) by A1, FINSUB_1:def 5;
A2: for a, b being Element of PFuncs (V,C) st a in B & b in B & a c= b holds
a = b by A1, SUBSTLAT:5;
for x being set st x in X holds
x is finite by A1, Th1;
then X in { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) } by A2;
hence X in SubstitutionSet (V,C) by SUBSTLAT:def 1; :: thesis: verum