let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable
for Sub being CQC_Substitution holds ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub]))
let x be bound_QC-variable; :: thesis: for Sub being CQC_Substitution holds ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub]))
let Sub be CQC_Substitution; :: thesis: ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub]))
set finSub = RestrictSub (x,(All (x,p)),Sub);

A1: now

reconsider F = {[x,(x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p)))]} as Function ;
dom F = {x} by RELAT_1:9;
then dom (RestrictSub (x,(All (x,p)),Sub)) misses dom F by Th6;
then dom (@ (RestrictSub (x,(All (x,p)),Sub))) misses dom F by SUBSTUT1:def 2;
then A2: (@ (RestrictSub (x,(All (x,p)),Sub))) \/ F = (@ (RestrictSub (x,(All (x,p)),Sub))) +* F by FUNCT_4:31;
assume A3: x in rng (RestrictSub (x,(All (x,p)),Sub)) ; :: thesis: ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub]))
then ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (RestrictSub (x,(All (x,p)),Sub)) \/ F by SUBSTUT1:def 13;
then ( {[x,(x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p)))]} = x .--> (x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p))) & ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* F ) by A2, FUNCT_4:82, SUBSTUT1:def 2;
hence ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) by A3, Th7; :: thesis: verum

end;

now

reconsider F = {[x,x]} as Function ;
dom F = {x} by RELAT_1:9;
then dom (RestrictSub (x,(All (x,p)),Sub)) misses dom F by Th6;
then dom (@ (RestrictSub (x,(All (x,p)),Sub))) misses dom F by SUBSTUT1:def 2;
then A4: (@ (RestrictSub (x,(All (x,p)),Sub))) \/ F = (@ (RestrictSub (x,(All (x,p)),Sub))) +* F by FUNCT_4:31;
assume A5: not x in rng (RestrictSub (x,(All (x,p)),Sub)) ; :: thesis: ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub]))
then ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (RestrictSub (x,(All (x,p)),Sub)) \/ F by SUBSTUT1:def 13;
then ( {[x,x]} = x .--> x & ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* F ) by A4, FUNCT_4:82, SUBSTUT1:def 2;
hence ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) by A5, Th8; :: thesis: verum

end;

hence ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) by A1; :: thesis: verum