let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for Sub being CQC_Substitution of Al holds dom (@ (RestrictSub (x,p,Sub))) misses (dom ((@ Sub) | (RSub1 p))) \/ (dom ((@ Sub) | (RSub2 (p,Sub))))
let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al
for Sub being CQC_Substitution of Al holds dom (@ (RestrictSub (x,p,Sub))) misses (dom ((@ Sub) | (RSub1 p))) \/ (dom ((@ Sub) | (RSub2 (p,Sub))))
let x be bound_QC-variable of Al; :: thesis: for Sub being CQC_Substitution of Al holds dom (@ (RestrictSub (x,p,Sub))) misses (dom ((@ Sub) | (RSub1 p))) \/ (dom ((@ Sub) | (RSub2 (p,Sub))))
let Sub be CQC_Substitution of Al; :: thesis: dom (@ (RestrictSub (x,p,Sub))) misses (dom ((@ Sub) | (RSub1 p))) \/ (dom ((@ Sub) | (RSub2 (p,Sub))))
set X = { y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ;
A1: dom ((@ Sub) | (RSub2 (p,Sub))) = (dom (@ Sub)) /\ (RSub2 (p,Sub)) by RELAT_1:61;
RestrictSub (x,p,Sub) = Sub | { y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } by SUBSTUT1:def 6;
then RestrictSub (x,p,Sub) = (@ Sub) | { y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } by SUBSTUT1:def 2;
then dom (@ (RestrictSub (x,p,Sub))) = dom ((@ Sub) | { y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ) by SUBSTUT1:def 2;
then A2: dom (@ (RestrictSub (x,p,Sub))) = (dom (@ Sub)) /\ { y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } by RELAT_1:61;
A3: dom ((@ Sub) | (RSub1 p)) = (dom (@ Sub)) /\ (RSub1 p) by RELAT_1:61;

now :: thesis: not dom (@ (RestrictSub (x,p,Sub))) meets (dom ((@ Sub) | (RSub1 p))) \/ (dom ((@ Sub) | (RSub2 (p,Sub))))

assume dom (@ (RestrictSub (x,p,Sub))) meets (dom ((@ Sub) | (RSub1 p))) \/ (dom ((@ Sub) | (RSub2 (p,Sub)))) ; :: thesis: contradiction
then consider b being object such that
A4: b in dom (@ (RestrictSub (x,p,Sub))) and
A5: b in (dom ((@ Sub) | (RSub1 p))) \/ (dom ((@ Sub) | (RSub2 (p,Sub)))) by XBOOLE_0:3;
b in { y where y is bound_QC-variable of Al : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } by A2, A4, XBOOLE_0:def 4;
then A6: ex y being bound_QC-variable of Al st
( b = y & y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) ;

A7: now :: thesis: not b in dom ((@ Sub) | (RSub2 (p,Sub)))

assume b in dom ((@ Sub) | (RSub2 (p,Sub))) ; :: thesis: contradiction
then b in RSub2 (p,Sub) by A1, XBOOLE_0:def 4;
then ex y1 being bound_QC-variable of Al st
( y1 = b & y1 in still_not-bound_in p & y1 = (@ Sub) . y1 ) by Def10;
hence contradiction by A6, SUBSTUT1:def 2; :: thesis: verum

end;

now :: thesis: not b in dom ((@ Sub) | (RSub1 p))

assume b in dom ((@ Sub) | (RSub1 p)) ; :: thesis: contradiction
then b in RSub1 p by A3, XBOOLE_0:def 4;
then ex y1 being bound_QC-variable of Al st
( y1 = b & not y1 in still_not-bound_in p ) by Def9;
hence contradiction by A6; :: thesis: verum

end;

hence contradiction by A5, A7, XBOOLE_0:def 3; :: thesis: verum

end;

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