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 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 A2: 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 ) }
consider i being Element of NAT , p being Element of CQC-WFF such that
A3: ( i in dom f & p = f . i & b in still_not-bound_in p ) by A2, 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 A3;
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 A3, TARSKI:def 4; :: thesis: verum

end;

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 A4: 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
consider Y being set such that
A5: ( b in Y & 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 A4, TARSKI:def 4;
S₁[Y] by A5;
hence b in still_not-bound_in f by A5, Def5; :: 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:2; :: thesis: verum