let p be Element of CQC-WFF ; :: thesis: for x, y being bound_QC-variable holds QuantNbr p = QuantNbr (p . x,y)
let x, y be bound_QC-variable; :: 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 2; :: thesis: verum