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

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