let S1, S2 be Element of QC-Sub-WFF ; :: thesis: ( S1 `2 = S2 `2 implies CQC_Sub (Sub_& S1,S2) = (CQC_Sub S1) '&' (CQC_Sub S2) )
assume A1: S1 `2 = S2 `2 ; :: thesis: CQC_Sub (Sub_& S1,S2) = (CQC_Sub S1) '&' (CQC_Sub S2)
set S = Sub_& S1,S2;
( Sub_the_left_argument_of (Sub_& S1,S2) = S1 & Sub_the_right_argument_of (Sub_& S1,S2) = S2 ) by A1, Th18, Th19;
hence CQC_Sub (Sub_& S1,S2) = (CQC_Sub S1) '&' (CQC_Sub S2) by A1, Th13, Th30; :: thesis: verum