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,(All (x,p)),Sub)) misses {x}
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,(All (x,p)),Sub)) misses {x}
let x be bound_QC-variable of Al; :: thesis: for Sub being CQC_Substitution of Al holds dom (RestrictSub (x,(All (x,p)),Sub)) misses {x}
let Sub be CQC_Substitution of Al; :: thesis: dom (RestrictSub (x,(All (x,p)),Sub)) misses {x}
set finSub = RestrictSub (x,(All (x,p)),Sub);

now :: thesis: not dom (RestrictSub (x,(All (x,p)),Sub)) meets {x}

set q = All (x,p);
set X = { y1 where y1 is bound_QC-variable of Al : ( y1 in still_not-bound_in (All (x,p)) & y1 is Element of dom Sub & y1 <> x & y1 <> Sub . y1 ) } ;
assume dom (RestrictSub (x,(All (x,p)),Sub)) meets {x} ; :: thesis: contradiction
then consider b being object such that
A1: b in dom (RestrictSub (x,(All (x,p)),Sub)) and
A2: b in {x} by XBOOLE_0:3;
RestrictSub (x,(All (x,p)),Sub) = Sub | { y1 where y1 is bound_QC-variable of Al : ( 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 of Al : ( 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 of Al : ( 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 of Al : ( y1 in still_not-bound_in (All (x,p)) & y1 is Element of dom Sub & y1 <> x & y1 <> Sub . y1 ) } by RELAT_1:61;
then A3: dom (@ (RestrictSub (x,(All (x,p)),Sub))) c= { y1 where y1 is bound_QC-variable of Al : ( 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 of Al : ( y1 in still_not-bound_in (All (x,p)) & y1 is Element of dom Sub & y1 <> x & y1 <> Sub . y1 ) } by A3;
then ex y being bound_QC-variable of Al st
( y = b & y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y ) ;
hence contradiction by A2, TARSKI:def 1; :: thesis: verum

end;

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