let A be QC-alphabet ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: still_not-bound_in (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {x}
let y be object ; :: 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 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))) ; :: 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 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;
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:3;
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:3;
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;