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;
set z = S_Bound [(All x,p),Sub];

A1: now

assume A2: 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]))
A3: {[x,(x. (upVar (RestrictSub x,(All x,p),Sub),p))]} = x .--> (x. (upVar (RestrictSub x,(All x,p),Sub),p)) by FUNCT_4:87;
reconsider F = {[x,(x. (upVar (RestrictSub x,(All x,p),Sub),p))]} as Function ;
dom F = {x} by RELAT_1:23;
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:32;
consider Sub1 being CQC_Substitution;
ExpandSub x,p,(RestrictSub x,(All x,p),Sub) = (RestrictSub x,(All x,p),Sub) \/ F by A2, SUBSTUT1:def 13;
then ExpandSub x,p,(RestrictSub x,(All x,p),Sub) = (@ (RestrictSub x,(All x,p),Sub)) +* F by A4, 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 A2, A3, Th7; :: thesis: verum

end;

now

assume A6: 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]))
A7: {[x,x]} = x .--> x by FUNCT_4:87;
reconsider F = {[x,x]} as Function ;
dom F = {x} by RELAT_1:23;
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 A8: (@ (RestrictSub x,(All x,p),Sub)) \/ F = (@ (RestrictSub x,(All x,p),Sub)) +* F by FUNCT_4:32;
ExpandSub x,p,(RestrictSub x,(All x,p),Sub) = (RestrictSub x,(All x,p),Sub) \/ F by A6, SUBSTUT1:def 13;
then ExpandSub x,p,(RestrictSub x,(All x,p),Sub) = (@ (RestrictSub x,(All x,p),Sub)) +* F by A8, 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 A6, A7, 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