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