let Al be QC-alphabet ; 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; 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; 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; 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 ( 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))
;
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;
verum end;
now ( 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))
;
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;
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; verum