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 not x in rng (RestrictSub (x,(All (x,p)),Sub)) holds

S_Bound [(All (x,p)),Sub] = x

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 not x in rng (RestrictSub (x,(All (x,p)),Sub)) holds

S_Bound [(All (x,p)),Sub] = x

let x be bound_QC-variable of Al; :: thesis: for Sub being CQC_Substitution of Al st not x in rng (RestrictSub (x,(All (x,p)),Sub)) holds

S_Bound [(All (x,p)),Sub] = x

let Sub be CQC_Substitution of Al; :: thesis: ( not x in rng (RestrictSub (x,(All (x,p)),Sub)) implies S_Bound [(All (x,p)),Sub] = x )

set finSub = RestrictSub (x,(All (x,p)),Sub);

set S = [(All (x,p)),Sub];

assume A1: not x in rng (RestrictSub (x,(All (x,p)),Sub)) ; :: thesis: S_Bound [(All (x,p)),Sub] = x

reconsider q = [(All (x,p)),Sub] `1 as Element of CQC-WFF Al ;

( [(All (x,p)),Sub] `2 = Sub & bound_in q = x ) by QC_LANG2:7;

hence S_Bound [(All (x,p)),Sub] = x by A1, SUBSTUT1:def 36; :: thesis: verum

for x being bound_QC-variable of Al

for Sub being CQC_Substitution of Al st not x in rng (RestrictSub (x,(All (x,p)),Sub)) holds

S_Bound [(All (x,p)),Sub] = x

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 not x in rng (RestrictSub (x,(All (x,p)),Sub)) holds

S_Bound [(All (x,p)),Sub] = x

let x be bound_QC-variable of Al; :: thesis: for Sub being CQC_Substitution of Al st not x in rng (RestrictSub (x,(All (x,p)),Sub)) holds

S_Bound [(All (x,p)),Sub] = x

let Sub be CQC_Substitution of Al; :: thesis: ( not x in rng (RestrictSub (x,(All (x,p)),Sub)) implies S_Bound [(All (x,p)),Sub] = x )

set finSub = RestrictSub (x,(All (x,p)),Sub);

set S = [(All (x,p)),Sub];

assume A1: not x in rng (RestrictSub (x,(All (x,p)),Sub)) ; :: thesis: S_Bound [(All (x,p)),Sub] = x

reconsider q = [(All (x,p)),Sub] `1 as Element of CQC-WFF Al ;

( [(All (x,p)),Sub] `2 = Sub & bound_in q = x ) by QC_LANG2:7;

hence S_Bound [(All (x,p)),Sub] = x by A1, SUBSTUT1:def 36; :: thesis: verum