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:19
.= 'not' (All (x,(('not' p) . y))) by A1, CQC_LANG:25
.= 'not' (All (x,('not' (p . y)))) by CQC_LANG:19
.= Ex (x,(p . y)) by QC_LANG2:def 5 ; :: thesis: verum