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