theorem Th16: :: QC_TRANS:16

for Al being QC-alphabet
for Al2 being b₁ -expanding QC-alphabet
for Z being Element of CQC-Sub-WFF Al
for Z2 being Element of CQC-Sub-WFF Al2 st Z `1 is universal & Z2 `1 is universal & bound_in (Z `1) = bound_in (Z2 `1) & the_scope_of (Z `1) = the_scope_of (Z2 `1) & Z = Z2 holds
S_Bound (@ Z) = S_Bound (@ Z2)