let Al be QC-alphabet ; :: thesis: 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])
let p, q be Element of CQC-WFF Al; :: thesis: for Sub being CQC_Substitution of Al holds [(p '&' q),Sub] = CQCSub_& ([p,Sub],[q,Sub])
let Sub be CQC_Substitution of Al; :: 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 ) ;
A2: ( [p,Sub] `2 = Sub & [q,Sub] `2 = Sub ) ;
then CQCSub_& ([p,Sub],[q,Sub]) = Sub_& ([p,Sub],[q,Sub]) by SUBLEMMA:def 3;
hence [(p '&' q),Sub] = CQCSub_& ([p,Sub],[q,Sub]) by A2, A1, SUBSTUT1:def 21; :: thesis: verum