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