let p, q be Element of CQC-WFF ; :: thesis: for x, y being bound_QC-variable 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; :: 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 '&' q),(Sbst x,y)] = CQCSub_& [p,(Sbst x,y)],[q,(Sbst x,y)] by Th19;
A2: ( [p,(Sbst x,y)] `2 = Sbst x,y & [q,(Sbst x,y)] `2 = Sbst x,y ) by MCART_1:7;
then A3: [(p '&' q),(Sbst x,y)] = Sub_& [p,(Sbst x,y)],[q,(Sbst x,y)] by A1, SUBLEMMA:def 4;
then A4: (p '&' q) . x,y = (CQC_Sub [p,(Sbst x,y)]) '&' (CQC_Sub [q,(Sbst x,y)]) by A2, 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 A5: ( 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 A4, CQC_SIM1:17;
hence QuantNbr (p '&' q) = QuantNbr ((p '&' q) . x,y) by A5, 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 A2, A3, SUBSTUT1:31; :: thesis: verum