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_{1}[ 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 ) } ;

( i in dom f & p = f . i ) } by A1, TARSKI:2; :: thesis: verum

( 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

( $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

( 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_{1}[Y]
by A3;

hence b in still_not-bound_in f by A2, Def5; :: thesis: verum

end;( 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

hence b in still_not-bound_in f by A2, Def5; :: thesis: verum

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 ) }

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 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;( 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

( i in dom f & p = f . i ) } by A1, TARSKI:2; :: thesis: verum