let p be Element of CQC-WFF ; :: thesis: for Sub being CQC_Substitution holds dom ((@ Sub) | (RSub1 p)) misses dom ((@ Sub) | (RSub2 p,Sub))
let Sub be CQC_Substitution; :: thesis: dom ((@ Sub) | (RSub1 p)) misses dom ((@ Sub) | (RSub2 p,Sub))

now

assume dom ((@ Sub) | (RSub1 p)) meets dom ((@ Sub) | (RSub2 p,Sub)) ; :: thesis: contradiction
then consider a being set 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:90;
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 a in (RSub1 p) /\ (RSub2 p,Sub) by XBOOLE_0:def 4;
then A2: ( a in RSub1 p & a in RSub2 p,Sub ) by XBOOLE_0:def 4;
then consider b being bound_QC-variable such that
A3: ( b = a & not b in still_not-bound_in p ) by Def11;
consider b being bound_QC-variable such that
A4: ( b = a & b in still_not-bound_in p & b = (@ Sub) . b ) by A2, Def12;
thus contradiction by A3, A4; :: thesis: verum

end;

hence dom ((@ Sub) | (RSub1 p)) misses dom ((@ Sub) | (RSub2 p,Sub)) ; :: thesis: verum