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 that
A1: b in SubstitutionSet (V,C) and
A2: a in b ; :: thesis: a is finite Function
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 A1, SUBSTLAT:def 1;
then 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 ) ) ;
hence a is finite Function by A1, A2; :: thesis: verum