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