let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable
for Sub being CQC_Substitution holds dom (@ (RestrictSub x,p,Sub)) misses (dom ((@ Sub) | (RSub1 p))) \/ (dom ((@ Sub) | (RSub2 p,Sub)))
let x be bound_QC-variable; :: thesis: for Sub being CQC_Substitution holds dom (@ (RestrictSub x,p,Sub)) misses (dom ((@ Sub) | (RSub1 p))) \/ (dom ((@ Sub) | (RSub2 p,Sub)))
let Sub be CQC_Substitution; :: 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 : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ;
RestrictSub x,p,Sub = Sub | { y where y is bound_QC-variable : ( 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 : ( 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 : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ) by SUBSTUT1:def 2;
then A1: ( dom (@ (RestrictSub x,p,Sub)) = (dom (@ Sub)) /\ { y where y is bound_QC-variable : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } & dom ((@ Sub) | (RSub1 p)) = (dom (@ Sub)) /\ (RSub1 p) & dom ((@ Sub) | (RSub2 p,Sub)) = (dom (@ Sub)) /\ (RSub2 p,Sub) ) by RELAT_1:90;

now

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

A4: now

assume b in dom ((@ Sub) | (RSub1 p)) ; :: thesis: contradiction
then b in RSub1 p by A1, XBOOLE_0:def 4;
then consider y1 being bound_QC-variable such that
A5: ( y1 = b & not y1 in still_not-bound_in p ) by Def11;
thus contradiction by A3, A5; :: thesis: verum

end;

now

assume b in dom ((@ Sub) | (RSub2 p,Sub)) ; :: thesis: contradiction
then b in RSub2 p,Sub by A1, XBOOLE_0:def 4;
then consider y1 being bound_QC-variable such that
A6: ( y1 = b & y1 in still_not-bound_in p & y1 = (@ Sub) . y1 ) by Def12;
thus contradiction by A3, A6, SUBSTUT1:def 2; :: thesis: verum

end;

hence contradiction by A2, A4, 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