consider p being Element of QC-WFF , Sub being CQC_Substitution such that
A1: S = [p,Sub] by SUBSTUT1:8;
thus S `2 is CQC_Substitution by A1, MCART_1:7; :: thesis: verum