let p, q be Element of CQC-WFF ; :: thesis: for Sub being CQC_Substitution holds [(p '&' q),Sub] = CQCSub_& [p,Sub],[q,Sub]
let Sub be CQC_Substitution; :: thesis: [(p '&' q),Sub] = CQCSub_& [p,Sub],[q,Sub]
set S1 = [p,Sub];
set S2 = [q,Sub];
A1: ( [p,Sub] `1 = p & [q,Sub] `1 = q ) by MCART_1:7;
A2: ( [p,Sub] `2 = Sub & [q,Sub] `2 = Sub ) by MCART_1:7;
then CQCSub_& [p,Sub],[q,Sub] = Sub_& [p,Sub],[q,Sub] by SUBLEMMA:def 4;
hence [(p '&' q),Sub] = CQCSub_& [p,Sub],[q,Sub] by A2, A1, SUBSTUT1:def 21; :: thesis: verum