let V, V', C, C' be set ; :: thesis: ( V c= V' & C c= C' implies SubstitutionSet V,C c= SubstitutionSet V',C' )
assume A1: ( V c= V' & C c= C' ) ; :: thesis: SubstitutionSet V,C c= SubstitutionSet V',C'
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 ) & ( for s, t being Element of PFuncs V,C st s in B & t in B & s c= t holds
s = t ) ) ;
A3: B in Fin (PFuncs V,C) ;
A4: B c= PFuncs V,C by FINSUB_1:def 5;
PFuncs V,C c= PFuncs V',C' by A1, PARTFUN1:128;
then Fin (PFuncs V,C) c= Fin (PFuncs V',C') by FINSUB_1:23;
then reconsider B = B as Element of Fin (PFuncs V',C') by A3;
for s, t being Element of PFuncs V',C' st s in B & t in B & s c= t holds
s = t by A2, A4;
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