let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for Sub being CQC_Substitution of Al holds dom ((@ Sub) | (RSub1 p)) misses dom ((@ Sub) | (RSub2 (p,Sub)))
let p be Element of CQC-WFF Al; :: thesis: for Sub being CQC_Substitution of Al holds dom ((@ Sub) | (RSub1 p)) misses dom ((@ Sub) | (RSub2 (p,Sub)))
let Sub be CQC_Substitution of Al; :: thesis: dom ((@ Sub) | (RSub1 p)) misses dom ((@ Sub) | (RSub2 (p,Sub)))
now :: thesis: not dom ((@ Sub) | (RSub1 p)) meets dom ((@ Sub) | (RSub2 (p,Sub)))
assume dom ((@ Sub) | (RSub1 p)) meets dom ((@ Sub) | (RSub2 (p,Sub))) ; :: thesis: contradiction
then consider a being object such that
A1: a in (dom ((@ Sub) | (RSub1 p))) /\ (dom ((@ Sub) | (RSub2 (p,Sub)))) by XBOOLE_0:4;
( dom ((@ Sub) | (RSub1 p)) = (dom (@ Sub)) /\ (RSub1 p) & dom ((@ Sub) | (RSub2 (p,Sub))) = (dom (@ Sub)) /\ (RSub2 (p,Sub)) ) by RELAT_1:61;
then a in ((dom (@ Sub)) /\ ((dom (@ Sub)) /\ (RSub1 p))) /\ (RSub2 (p,Sub)) by A1, XBOOLE_1:16;
then a in (((dom (@ Sub)) /\ (dom (@ Sub))) /\ (RSub1 p)) /\ (RSub2 (p,Sub)) by XBOOLE_1:16;
then a in (dom (@ Sub)) /\ ((RSub1 p) /\ (RSub2 (p,Sub))) by XBOOLE_1:16;
then A2: a in (RSub1 p) /\ (RSub2 (p,Sub)) by XBOOLE_0:def 4;
then a in RSub2 (p,Sub) by XBOOLE_0:def 4;
then A3: ex b being bound_QC-variable of Al st
( b = a & b in still_not-bound_in p & b = (@ Sub) . b ) by Def10;
a in RSub1 p by A2, XBOOLE_0:def 4;
then ex b being bound_QC-variable of Al st
( b = a & not b in still_not-bound_in p ) by Def9;
hence contradiction by A3; :: thesis: verum
end;
hence dom ((@ Sub) | (RSub1 p)) misses dom ((@ Sub) | (RSub2 (p,Sub))) ; :: thesis: verum