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 A2: a in still_not-bound_in (rng f) ; :: thesis: a in still_not-bound_in f
consider b being set such that
A3: ( a in b & b in { (still_not-bound_in p) where p is Element of CQC-WFF : p in rng f } ) by A2, TARSKI:def 4;
consider p being Element of CQC-WFF such that
A4: ( b = still_not-bound_in p & p in rng f ) by A3;
consider c being set such that
A5: ( c in dom f & f . c = p ) by A4, FUNCT_1:def 5;
thus a in still_not-bound_in f by A3, A4, A5, 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 A6: a in still_not-bound_in f ; :: thesis: a in still_not-bound_in (rng f)
consider i being Element of NAT , q being Element of CQC-WFF such that
A7: ( i in dom f & q = f . i & a in still_not-bound_in q ) by A6, CALCUL_1:def 5;
q in rng f by A7, FUNCT_1:def 5;
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 A7, TARSKI:def 4; :: thesis: verum

end;

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