let f be FinSequence of CQC-WFF ; :: thesis: still_not-bound_in f = union { (still_not-bound_in p) where p is Element of CQC-WFF : ex i being Element of NAT st
( i in dom f & p = f . i ) }
defpred S₁[ set ] means ex p being Element of CQC-WFF st
( $1 = still_not-bound_in p & ex i being Element of NAT st
( i in dom f & p = f . i ) );
set X = { (still_not-bound_in p) where p is Element of CQC-WFF : ex i being Element of NAT st
( i in dom f & p = f . i ) } ;

A1: now

let b be set ; :: thesis: ( b in union { (still_not-bound_in p) where p is Element of CQC-WFF : ex i being Element of NAT st
( i in dom f & p = f . i ) } implies b in still_not-bound_in f )
assume b in union { (still_not-bound_in p) where p is Element of CQC-WFF : ex i being Element of NAT st
( i in dom f & p = f . i ) } ; :: thesis: b in still_not-bound_in f
then consider Y being set such that
A2: b in Y and
A3: Y in { (still_not-bound_in p) where p is Element of CQC-WFF : ex i being Element of NAT st
( i in dom f & p = f . i ) } by TARSKI:def 4;
S₁[Y] by A3;
hence b in still_not-bound_in f by A2, Def5; :: thesis: verum

end;

now

let b be set ; :: thesis: ( b in still_not-bound_in f implies b in union { (still_not-bound_in p) where p is Element of CQC-WFF : ex i being Element of NAT st
( i in dom f & p = f . i ) } )
assume b in still_not-bound_in f ; :: thesis: b in union { (still_not-bound_in p) where p is Element of CQC-WFF : ex i being Element of NAT st
( i in dom f & p = f . i ) }
then consider i being Element of NAT , p being Element of CQC-WFF such that
A4: ( i in dom f & p = f . i ) and
A5: b in still_not-bound_in p by Def5;
still_not-bound_in p in { (still_not-bound_in p) where p is Element of CQC-WFF : ex i being Element of NAT st
( i in dom f & p = f . i ) } by A4;
hence b in union { (still_not-bound_in p) where p is Element of CQC-WFF : ex i being Element of NAT st
( i in dom f & p = f . i ) } by A5, TARSKI:def 4; :: thesis: verum

end;

hence still_not-bound_in f = union { (still_not-bound_in p) where p is Element of CQC-WFF : ex i being Element of NAT st
( i in dom f & p = f . i ) } by A1, TARSKI:1; :: thesis: verum