let p, q be Element of CQC-WFF ; :: thesis: ( ( for Sub being CQC_Substitution holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) & ( for Sub being CQC_Substitution holds QuantNbr q = QuantNbr (CQC_Sub [q,Sub]) ) implies for Sub being CQC_Substitution holds QuantNbr (p '&' q) = QuantNbr (CQC_Sub [(p '&' q),Sub]) )
assume A1: ( ( for Sub being CQC_Substitution holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) & ( for Sub being CQC_Substitution holds QuantNbr q = QuantNbr (CQC_Sub [q,Sub]) ) ) ; :: thesis: for Sub being CQC_Substitution holds QuantNbr (p '&' q) = QuantNbr (CQC_Sub [(p '&' q),Sub])
let Sub be CQC_Substitution; :: thesis: QuantNbr (p '&' q) = QuantNbr (CQC_Sub [(p '&' q),Sub])
set S = [(p '&' q),Sub];
set S1 = [p,Sub];
set S2 = [q,Sub];
A2: [(p '&' q),Sub] = CQCSub_& [p,Sub],[q,Sub] by Th19;
A3: ( [p,Sub] `2 = Sub & [q,Sub] `2 = Sub ) by MCART_1:7;
then [(p '&' q),Sub] = Sub_& [p,Sub],[q,Sub] by A2, SUBLEMMA:def 4;
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 A1 ;
hence QuantNbr (p '&' q) = QuantNbr (CQC_Sub [(p '&' q),Sub]) by CQC_SIM1:17; :: thesis: verum