let A be QC-alphabet ; :: thesis: for k being Nat
for l being QC-variable_list of k,A
for a being free_QC-variable of A
for x being bound_QC-variable of A holds still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x)))
let k be Nat; :: thesis: for l being QC-variable_list of k,A
for a being free_QC-variable of A
for x being bound_QC-variable of A holds still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x)))
let l be QC-variable_list of k,A; :: thesis: for a being free_QC-variable of A
for x being bound_QC-variable of A holds still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x)))
let a be free_QC-variable of A; :: thesis: for x being bound_QC-variable of A holds still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x)))
let x be bound_QC-variable of A; :: thesis: still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x)))
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in still_not-bound_in l or y in still_not-bound_in (Subst (l,(a .--> x))) )
A1: still_not-bound_in l = { (l . n) where n is Nat : ( 1 <= n & n <= len l & l . n in bound_QC-variables A ) } by QC_LANG1:def 29;
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 Nat : ( 1 <= n & n <= len (Subst (l,(a .--> x))) & (Subst (l,(a .--> x))) . n in bound_QC-variables A ) } by QC_LANG1:def 29;
consider n being Nat such that
A4: y9 = l . n and
A5: 1 <= n and
A6: n <= len l and
A7: l . n in bound_QC-variables A 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