let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable
for Sub being CQC_Substitution holds dom (RestrictSub x,(All x,p),Sub) misses {x}
let x be bound_QC-variable; :: thesis: for Sub being CQC_Substitution holds dom (RestrictSub x,(All x,p),Sub) misses {x}
let Sub be CQC_Substitution; :: thesis: dom (RestrictSub x,(All x,p),Sub) misses {x}
set finSub = RestrictSub x,(All x,p),Sub;

now

assume dom (RestrictSub x,(All x,p),Sub) meets {x} ; :: thesis: contradiction
then consider b being set such that
A1: ( b in dom (RestrictSub x,(All x,p),Sub) & b in {x} ) by XBOOLE_0:3;
set q = All x,p;
set X = { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All x,p) & y1 is Element of dom Sub & y1 <> x & y1 <> Sub . y1 ) } ;
RestrictSub x,(All x,p),Sub = Sub | { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All x,p) & y1 is Element of dom Sub & y1 <> x & y1 <> Sub . y1 ) } by SUBSTUT1:def 6;
then RestrictSub x,(All x,p),Sub = (@ Sub) | { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All x,p) & y1 is Element of dom Sub & y1 <> x & y1 <> Sub . y1 ) } by SUBSTUT1:def 2;
then @ (RestrictSub x,(All x,p),Sub) = (@ Sub) | { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All x,p) & y1 is Element of dom Sub & y1 <> x & y1 <> Sub . y1 ) } by SUBSTUT1:def 2;
then dom (@ (RestrictSub x,(All x,p),Sub)) = (dom (@ Sub)) /\ { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All x,p) & y1 is Element of dom Sub & y1 <> x & y1 <> Sub . y1 ) } by RELAT_1:90;
then A2: dom (@ (RestrictSub x,(All x,p),Sub)) c= { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All x,p) & y1 is Element of dom Sub & y1 <> x & y1 <> Sub . y1 ) } by XBOOLE_1:17;
b in dom (@ (RestrictSub x,(All x,p),Sub)) by A1, SUBSTUT1:def 2;
then b in { y1 where y1 is bound_QC-variable : ( y1 in still_not-bound_in (All x,p) & y1 is Element of dom Sub & y1 <> x & y1 <> Sub . y1 ) } by A2;
then consider y being bound_QC-variable such that
A3: ( y = b & y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) ;
thus contradiction by A1, A3, TARSKI:def 1; :: thesis: verum

end;

hence dom (RestrictSub x,(All x,p),Sub) misses {x} ; :: thesis: verum