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 st x in rng (RestrictSub (x,(All (x,p)),Sub)) holds
S_Bound [(All (x,p)),Sub] = x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p))
let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al
for Sub being CQC_Substitution of Al st x in rng (RestrictSub (x,(All (x,p)),Sub)) holds
S_Bound [(All (x,p)),Sub] = x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p))
let x be bound_QC-variable of Al; :: thesis: for Sub being CQC_Substitution of Al st x in rng (RestrictSub (x,(All (x,p)),Sub)) holds
S_Bound [(All (x,p)),Sub] = x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p))
let Sub be CQC_Substitution of Al; :: thesis: ( x in rng (RestrictSub (x,(All (x,p)),Sub)) implies S_Bound [(All (x,p)),Sub] = x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p)) )
set finSub = RestrictSub (x,(All (x,p)),Sub);
set S = [(All (x,p)),Sub];
assume A1: x in rng (RestrictSub (x,(All (x,p)),Sub)) ; :: thesis: S_Bound [(All (x,p)),Sub] = x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p))
reconsider q = [(All (x,p)),Sub] `1 as Element of CQC-WFF Al ;
A2: [(All (x,p)),Sub] `2 = Sub ;
( bound_in q = x & the_scope_of q = p ) by QC_LANG2:7;
hence S_Bound [(All (x,p)),Sub] = x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p)) by A1, A2, SUBSTUT1:def 36; :: thesis: verum