theorem Th7: :: GOEDCPUC:7

for Al being QC-alphabet
for Al2 being b₁ -expanding QC-alphabet
for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds
( Al2 -Cast (r 'or' s) = (Al2 -Cast r) 'or' (Al2 -Cast s) & Al2 -Cast (Ex (x,r)) = Ex ((Al2 -Cast x),(Al2 -Cast r)) )