let Al be QC-alphabet ; :: thesis: for S1, S2 being Element of CQC-Sub-WFF Al st S1 `2 = S2 `2 holds
CQC_Sub (CQCSub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2)
let S1, S2 be Element of CQC-Sub-WFF Al; :: thesis: ( S1 `2 = S2 `2 implies CQC_Sub (CQCSub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2) )
assume A1: S1 `2 = S2 `2 ; :: thesis: CQC_Sub (CQCSub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2)
then CQCSub_& (S1,S2) = Sub_& (S1,S2) by Def3;
hence CQC_Sub (CQCSub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2) by A1, SUBSTUT1:31; :: thesis: verum