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 ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub]))
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 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 of Al; :: thesis: for Sub being CQC_Substitution of Al 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 of Al; :: 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 :: thesis: ( x in rng (RestrictSub (x,(All (x,p)),Sub)) implies ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) )

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 :: thesis: ( not x in rng (RestrictSub (x,(All (x,p)),Sub)) implies ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) )

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