let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable
for Sub being CQC_Substitution 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; :: thesis: for Sub being CQC_Substitution st not x in rng (RestrictSub (x,(All (x,p)),Sub)) holds
S_Bound [(All (x,p)),Sub] = x
let Sub be CQC_Substitution; :: 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 by MCART_1:7;
A2: [(All (x,p)),Sub] `1 = All (x,p) by MCART_1:7;
then ( [(All (x,p)),Sub] `2 = Sub & bound_in q = x ) by MCART_1:7, QC_LANG2:8;
hence S_Bound [(All (x,p)),Sub] = x by A1, A2, SUBSTUT1:def 36; :: thesis: verum