let V, C be set ; :: thesis: for a, b being set st b in SubstitutionSet V,C & a in b holds
a is finite
let a, b be set ; :: thesis: ( b in SubstitutionSet V,C & a in b implies a is finite )
assume A1: ( b in SubstitutionSet V,C & a in b ) ; :: thesis: a is finite
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 by A1, A2; :: thesis: verum