let V, C be set ; :: thesis: for a, b being set st b in SubstitutionSet V,C & a in b holds
a is finite Function
let a, b be set ; :: thesis: ( b in SubstitutionSet V,C & a in b implies a is finite Function )
assume A1: ( b in SubstitutionSet V,C & a in b ) ; :: thesis: a is finite Function
then b in { A where A is Element of Fin (PFuncs V,C) : ( ( for u being set st u in A holds
u is finite ) & ( for s1, t being Element of PFuncs V,C st s1 in A & t in A & s1 c= t holds
s1 = t ) ) } by SUBSTLAT:def 1;
then consider A being Element of Fin (PFuncs V,C) such that
A2: ( A = b & ( 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 ) ) ;
thus a is finite Function by A1, A2; :: thesis: verum