let k be Element of NAT ; 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; 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; 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; still_not-bound_in l c= still_not-bound_in (Subst l,(a .--> x))
now let y be
set ;
( 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 28;
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 Element of NAT : ( 1 <= n & n <= len (Subst l,(a .--> x)) & (Subst l,(a .--> x)) . n in bound_QC-variables ) }
by QC_LANG1:def 28;
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:42;
then A8:
l . n = (Subst l,(a .--> x)) . n
by A5, A6, CQC_LANG:11;
n <= len (Subst l,(a .--> x))
by A6, CQC_LANG:def 3;
hence
y in still_not-bound_in (Subst l,(a .--> x))
by A3, A4, A5, A7, A8;
verum end;
hence
still_not-bound_in l c= still_not-bound_in (Subst l,(a .--> x))
by TARSKI:def 3; verum