let Al be QC-alphabet ; :: thesis: for f being FinSequence of CQC-WFF Al holds still_not-bound_in (rng f) = still_not-bound_in f
let f be FinSequence of CQC-WFF Al; :: thesis: still_not-bound_in (rng f) = still_not-bound_in f
set A = { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in rng f } ;

A1: now :: thesis: for a being object st a in still_not-bound_in (rng f) holds
a in still_not-bound_in f

let a be object ; :: thesis: ( a in still_not-bound_in (rng f) implies a in still_not-bound_in f )
assume a in still_not-bound_in (rng f) ; :: thesis: a in still_not-bound_in f
then consider b being set such that
A2: a in b and
A3: b in { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in rng f } by TARSKI:def 4;
consider p being Element of CQC-WFF Al such that
A4: b = still_not-bound_in p and
A5: p in rng f by A3;
ex c being object st
( c in dom f & f . c = p ) by A5, FUNCT_1:def 3;
hence a in still_not-bound_in f by A2, A4, CALCUL_1:def 5; :: thesis: verum

end;

now :: thesis: for a being object st a in still_not-bound_in f holds
a in still_not-bound_in (rng f)

let a be object ; :: thesis: ( a in still_not-bound_in f implies a in still_not-bound_in (rng f) )
assume a in still_not-bound_in f ; :: thesis: a in still_not-bound_in (rng f)
then consider i being Nat, q being Element of CQC-WFF Al such that
A6: i in dom f and
A7: q = f . i and
A8: a in still_not-bound_in q by CALCUL_1:def 5;
q in rng f by A6, A7, FUNCT_1:def 3;
then still_not-bound_in q in { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in rng f } ;
hence a in still_not-bound_in (rng f) by A8, TARSKI:def 4; :: thesis: verum

end;

hence still_not-bound_in (rng f) = still_not-bound_in f by A1, TARSKI:2; :: thesis: verum