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 (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {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 (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {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 (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {x}
let a be free_QC-variable of A; for x being bound_QC-variable of A holds still_not-bound_in (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {x}
let x be bound_QC-variable of A; still_not-bound_in (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {x}
let y be object ; TARSKI:def 3 ( not y in still_not-bound_in (Subst (l,(a .--> x))) or y in (still_not-bound_in l) \/ {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 (Subst (l,(a .--> x)))
; y in (still_not-bound_in l) \/ {x}
then reconsider y9 = y as Element of still_not-bound_in (Subst (l,(a .--> x))) ;
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;
then consider n being Nat such that
A3:
y9 = (Subst (l,(a .--> x))) . n
and
A4:
1 <= n
and
A5:
n <= len (Subst (l,(a .--> x)))
and
A6:
(Subst (l,(a .--> x))) . n in bound_QC-variables A
by A2;
A7:
n <= len l
by A5, CQC_LANG:def 1;