let k be Element of NAT ; :: thesis: for l being QC-variable_list of
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 ; :: 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;
A2: 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;
assume A3: y in still_not-bound_in (Subst l,(a .--> x)) ; :: thesis: y in (still_not-bound_in l) \/ {x}
then reconsider y' = y as Element of still_not-bound_in (Subst l,(a .--> x)) ;
consider n being Element of NAT such that
A4: y' = (Subst l,(a .--> x)) . n and
A5: 1 <= n and
A6: n <= len (Subst l,(a .--> x)) and
A7: (Subst l,(a .--> x)) . n in bound_QC-variables by A2, A3;
A8: n <= len l by A6, 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 y' = x by A4, A5, A8, CQC_LANG:11;
then y' 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 A5, A8, CQC_LANG:11;
then y' in still_not-bound_in l by A1, A4, A5, A7, A8;
hence y in (still_not-bound_in l) \/ {x} by XBOOLE_0:def 3; :: thesis: verum

end;

end;