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

consider Sub1 being CQC_Substitution;
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 A2: (@ (RestrictSub x,(All x,p),Sub)) \/ F = (@ (RestrictSub x,(All x,p),Sub)) +* F by FUNCT_4:32;
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:87, 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: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;
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:87, 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