let Al be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF Al
for x, y being bound_QC-variable of Al holds
( (p '&' q) . (x,y) = (p . (x,y)) '&' (q . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) & QuantNbr q = QuantNbr (q . (x,y)) implies QuantNbr (p '&' q) = QuantNbr ((p '&' q) . (x,y)) ) )
let p, q be Element of CQC-WFF Al; :: thesis: for x, y being bound_QC-variable of Al holds
( (p '&' q) . (x,y) = (p . (x,y)) '&' (q . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) & QuantNbr q = QuantNbr (q . (x,y)) implies QuantNbr (p '&' q) = QuantNbr ((p '&' q) . (x,y)) ) )
let x, y be bound_QC-variable of Al; :: thesis: ( (p '&' q) . (x,y) = (p . (x,y)) '&' (q . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) & QuantNbr q = QuantNbr (q . (x,y)) implies QuantNbr (p '&' q) = QuantNbr ((p '&' q) . (x,y)) ) )
set S = [(p '&' q),(Sbst (x,y))];
set S1 = [p,(Sbst (x,y))];
set S2 = [q,(Sbst (x,y))];
A1: ( [p,(Sbst (x,y))] `2 = Sbst (x,y) & [q,(Sbst (x,y))] `2 = Sbst (x,y) ) ;
[(p '&' q),(Sbst (x,y))] = CQCSub_& ([p,(Sbst (x,y))],[q,(Sbst (x,y))]) by Th19;
then A2: [(p '&' q),(Sbst (x,y))] = Sub_& ([p,(Sbst (x,y))],[q,(Sbst (x,y))]) by A1, SUBLEMMA:def 3;
then A3: (p '&' q) . (x,y) = (CQC_Sub [p,(Sbst (x,y))]) '&' (CQC_Sub [q,(Sbst (x,y))]) by A1, SUBSTUT1:31;
( QuantNbr p = QuantNbr (p . (x,y)) & QuantNbr q = QuantNbr (q . (x,y)) implies QuantNbr (p '&' q) = QuantNbr ((p '&' q) . (x,y)) )

proof

assume A4: ( QuantNbr p = QuantNbr (p . (x,y)) & QuantNbr q = QuantNbr (q . (x,y)) ) ; :: thesis: QuantNbr (p '&' q) = QuantNbr ((p '&' q) . (x,y))
QuantNbr ((p '&' q) . (x,y)) = (QuantNbr (p . (x,y))) + (QuantNbr (q . (x,y))) by A3, CQC_SIM1:17;
hence QuantNbr (p '&' q) = QuantNbr ((p '&' q) . (x,y)) by A4, CQC_SIM1:17; :: thesis: verum

end;

hence ( (p '&' q) . (x,y) = (p . (x,y)) '&' (q . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) & QuantNbr q = QuantNbr (q . (x,y)) implies QuantNbr (p '&' q) = QuantNbr ((p '&' q) . (x,y)) ) ) by A1, A2, SUBSTUT1:31; :: thesis: verum