let k be Element of NAT ; :: thesis: for l being QC-variable_list of k
for a being free_QC-variable
for x being bound_QC-variable holds still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x)))
let l be QC-variable_list of k; :: thesis: for a being free_QC-variable
for x being bound_QC-variable holds still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x)))
let a be free_QC-variable; :: thesis: for x being bound_QC-variable holds still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x)))
let x be bound_QC-variable; :: thesis: still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x)))

now

let y be set ; :: thesis: ( y in still_not-bound_in l implies y in still_not-bound_in (Subst (l,(a .--> x))) )
A1: still_not-bound_in l = { (l . n) where n is Element of NAT : ( 1 <= n & n <= len l & l . n in bound_QC-variables ) } by QC_LANG1:def 27;
assume A2: y in still_not-bound_in l ; :: thesis: y in still_not-bound_in (Subst (l,(a .--> x)))
then reconsider y9 = y as Element of still_not-bound_in l ;
A3: still_not-bound_in (Subst (l,(a .--> x))) = { ((Subst (l,(a .--> x))) . n) where n is Element of NAT : ( 1 <= n & n <= len (Subst (l,(a .--> x))) & (Subst (l,(a .--> x))) . n in bound_QC-variables ) } by QC_LANG1:def 27;
consider n being Element of NAT such that
A4: y9 = l . n and
A5: 1 <= n and
A6: n <= len l and
A7: l . n in bound_QC-variables by A1, A2;
l . n <> a by A7, QC_LANG3:34;
then A8: l . n = (Subst (l,(a .--> x))) . n by A5, A6, CQC_LANG:3;
n <= len (Subst (l,(a .--> x))) by A6, CQC_LANG:def 1;
hence y in still_not-bound_in (Subst (l,(a .--> x))) by A3, A4, A5, A7, A8; :: thesis: verum

end;

hence still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x))) by TARSKI:def 3; :: thesis: verum