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