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

A1: now :: thesis: for b being object st b in union { (still_not-bound_in p) where p is Element of CQC-WFF Al : ex i being Nat st
( i in dom f & p = f . i ) } holds
b in still_not-bound_in f

let b be object ; :: thesis: ( b in union { (still_not-bound_in p) where p is Element of CQC-WFF Al : ex i being 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 Al : ex i being 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 Al : ex i being 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 :: thesis: for b being object st b in still_not-bound_in f holds
b in union { (still_not-bound_in p) where p is Element of CQC-WFF Al : ex i being Nat st
( i in dom f & p = f . i ) }

let b be object ; :: thesis: ( b in still_not-bound_in f implies b in union { (still_not-bound_in p) where p is Element of CQC-WFF Al : ex i being 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 Al : ex i being Nat st
( i in dom f & p = f . i ) }
then consider i being Nat, p being Element of CQC-WFF Al 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 Al : ex i being 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 Al : ex i being 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 Al : ex i being Nat st
( i in dom f & p = f . i ) } by A1, TARSKI:2; :: thesis: verum