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 that
A1: b in SubstitutionSet (V,C) and
A2: a in b ; :: thesis: a is finite
ex A being Element of Fin (PFuncs (V,C)) st
( 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 ) ) by A1;
hence a is finite by A2; :: thesis: verum