let V, V', C, C' be set ; :: thesis: ( V c= V' & C c= C' implies SubstitutionSet V,C c= SubstitutionSet V',C' )
assume ( V c= V' & C c= C' ) ; :: thesis: SubstitutionSet V,C c= SubstitutionSet V',C'
then A1: PFuncs V,C c= PFuncs V',C' by PARTFUN1:128;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in SubstitutionSet V,C or x in SubstitutionSet V',C' )
assume x in SubstitutionSet V,C ; :: thesis: x in SubstitutionSet V',C'
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 SUBSTLAT:def 1;
then consider B being Element of Fin (PFuncs V,C) such that
A2: ( B = x & ( for u being set st u in B holds
u is finite ) ) and
A3: for s, t being Element of PFuncs V,C st s in B & t in B & s c= t holds
s = t ;
A4: ( B in Fin (PFuncs V,C) & Fin (PFuncs V,C) c= Fin (PFuncs V',C') ) by A1, FINSUB_1:23;
A5: B c= PFuncs V,C by FINSUB_1:def 5;
reconsider B = B as Element of Fin (PFuncs V',C') by A4;
for s, t being Element of PFuncs V',C' st s in B & t in B & s c= t holds
s = t by A3, A5;
then x in { D where D is Element of Fin (PFuncs V',C') : ( ( for u being set st u in D holds
u is finite ) & ( for s, t being Element of PFuncs V',C' st s in D & t in D & s c= t holds
s = t ) ) } by A2;
hence x in SubstitutionSet V',C' by SUBSTLAT:def 1; :: thesis: verum