theorem Th19: :: SUBSTUT2:19

for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for Sub being CQC_Substitution of Al holds [(p '&' q),Sub] = CQCSub_& ([p,Sub],[q,Sub])