let A be QC-alphabet ; 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; 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; 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; 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; still_not-bound_in l c= still_not-bound_in (Subst (l,(a .--> x)))
let y be object ; TARSKI:def 3 ( 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
; 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; verum