theorem Th15: :: QC_TRANS:15

for Al being QC-alphabet
for Al2 being b₁ -expanding QC-alphabet
for p2 being Element of CQC-WFF Al2
for S being CQC_Substitution of Al
for S2 being CQC_Substitution of Al2
for x2 being bound_QC-variable of Al2
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al st p = p2 & S = S2 & x = x2 holds
ExpandSub (x,p,(RestrictSub (x,(All (x,p)),S))) = ExpandSub (x2,p2,(RestrictSub (x2,(All (x2,p2)),S2)))