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 (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {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 (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {x}
let a be free_QC-variable; :: thesis: for x being bound_QC-variable holds still_not-bound_in (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {x}
let x be bound_QC-variable; :: thesis: still_not-bound_in (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {x}
let y be set ; :: according to TARSKI:def 3 :: thesis: ( 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 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 (Subst (l,(a .--> x))) ; :: thesis: 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 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;
then consider n being Element of 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 by A2;
A7: n <= len l by A5, CQC_LANG:def 3;

per cases ( l . n = a or l . n <> a ) ;

suppose l . n = a ; :: thesis: y in (still_not-bound_in l) \/ {x}

then y9 = x by A3, A4, A7, CQC_LANG:11;
then y9 in {x} by TARSKI:def 1;
hence y in (still_not-bound_in l) \/ {x} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose l . n <> a ; :: thesis: y in (still_not-bound_in l) \/ {x}

then l . n = (Subst (l,(a .--> x))) . n by A4, A7, CQC_LANG:11;
then y9 in still_not-bound_in l by A1, A3, A4, A6, A7;
hence y in (still_not-bound_in l) \/ {x} by XBOOLE_0:def 3; :: thesis: verum

end;

end;