let Al be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) & ( for Sub being CQC_Substitution of Al holds QuantNbr q = QuantNbr (CQC_Sub [q,Sub]) ) holds
for Sub being CQC_Substitution of Al holds QuantNbr (p '&' q) = QuantNbr (CQC_Sub [(p '&' q),Sub])
let p, q be Element of CQC-WFF Al; :: thesis: ( ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) & ( for Sub being CQC_Substitution of Al holds QuantNbr q = QuantNbr (CQC_Sub [q,Sub]) ) implies for Sub being CQC_Substitution of Al holds QuantNbr (p '&' q) = QuantNbr (CQC_Sub [(p '&' q),Sub]) )
assume that
A1: for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) and
A2: for Sub being CQC_Substitution of Al holds QuantNbr q = QuantNbr (CQC_Sub [q,Sub]) ; :: thesis: for Sub being CQC_Substitution of Al holds QuantNbr (p '&' q) = QuantNbr (CQC_Sub [(p '&' q),Sub])
let Sub be CQC_Substitution of Al; :: thesis: QuantNbr (p '&' q) = QuantNbr (CQC_Sub [(p '&' q),Sub])
set S = [(p '&' q),Sub];
set S1 = [p,Sub];
set S2 = [q,Sub];
A3: ( [p,Sub] `2 = Sub & [q,Sub] `2 = Sub ) ;
[(p '&' q),Sub] = CQCSub_& ([p,Sub],[q,Sub]) by Th19;
then [(p '&' q),Sub] = Sub_& ([p,Sub],[q,Sub]) by A3, SUBLEMMA:def 3;
then CQC_Sub [(p '&' q),Sub] = (CQC_Sub [p,Sub]) '&' (CQC_Sub [q,Sub]) by A3, SUBSTUT1:31;
then QuantNbr (CQC_Sub [(p '&' q),Sub]) = (QuantNbr (CQC_Sub [p,Sub])) + (QuantNbr (CQC_Sub [q,Sub])) by CQC_SIM1:17
.= (QuantNbr p) + (QuantNbr (CQC_Sub [q,Sub])) by A1
.= (QuantNbr p) + (QuantNbr q) by A2 ;
hence QuantNbr (p '&' q) = QuantNbr (CQC_Sub [(p '&' q),Sub]) by CQC_SIM1:17; :: thesis: verum