let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for x, y being bound_QC-variable of Al holds QuantNbr p = QuantNbr (p . (x,y))
let p be Element of CQC-WFF Al; :: thesis: for x, y being bound_QC-variable of Al holds QuantNbr p = QuantNbr (p . (x,y))
let x, y be bound_QC-variable of Al; :: thesis: QuantNbr p = QuantNbr (p . (x,y))
QuantNbr p = QuantNbr (CQC_Sub [p,(Sbst (x,y))]) by SUBSTUT2:25;
hence QuantNbr p = QuantNbr (p . (x,y)) by SUBSTUT2:def 1; :: thesis: verum