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);

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}

hence
dom (RestrictSub (x,(All (x,p)),Sub)) misses {x}
; :: thesis: verumset 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;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