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, XBOOLE_1:1;
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, Th2;
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