theorem Th8: :: QC_TRANS:8

for Al being QC-alphabet
for k being Nat
for p, r being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al
for Al2 being b₁ -expanding QC-alphabet holds
( Al2 -Cast (VERUM Al) = VERUM Al2 & Al2 -Cast (P ! l) = (Al2 -Cast P) ! (Al2 -Cast l) & Al2 -Cast ('not' p) = 'not' (Al2 -Cast p) & Al2 -Cast (p '&' r) = (Al2 -Cast p) '&' (Al2 -Cast r) & Al2 -Cast (All (x,p)) = All ((Al2 -Cast x),(Al2 -Cast p)) )