let p be Element of CQC-WFF ; :: thesis: for x, y being bound_QC-variable st x <> y holds
(Ex x,p) . y = Ex x,(p . y)
let x, y be bound_QC-variable; :: thesis: ( x <> y implies (Ex x,p) . y = Ex x,(p . y) )
assume A1: x <> y ; :: thesis: (Ex x,p) . y = Ex x,(p . y)
thus (Ex x,p) . y = ('not' (All x,('not' p))) . y by QC_LANG2:def 5
.= 'not' ((All x,('not' p)) . y) by CQC_LANG:32
.= 'not' (All x,(('not' p) . y)) by A1, CQC_LANG:38
.= 'not' (All x,('not' (p . y))) by CQC_LANG:32
.= Ex x,(p . y) by QC_LANG2:def 5 ; :: thesis: verum