let S1, S2 be Element of CQC-Sub-WFF ; :: 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, Def4;
hence ( (CQCSub_& S1,S2) `1 = (S1 `1 ) '&' (S2 `1 ) & (CQCSub_& S1,S2) `2 = S1 `2 ) by MCART_1:7; :: thesis: verum