let f be FinSequence of CQC-WFF ; :: 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 : p in rng f } ;

A1: now

let a be set ; :: 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 : p in rng f } by TARSKI:def 4;
consider p being Element of CQC-WFF such that
A4: b = still_not-bound_in p and
A5: p in rng f by A3;
ex c being set 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

let a be set ; :: 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 Element of NAT , q being Element of CQC-WFF 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 : 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:1; :: thesis: verum