let Al be QC-alphabet ; :: thesis: for f being FinSequence of CQC-WFF Al holds still_not-bound_in f is finite

let f be FinSequence of CQC-WFF Al; :: thesis: still_not-bound_in f is finite

defpred S_{1}[ object , object ] means ex p being Element of CQC-WFF Al st

( $2 = still_not-bound_in p & p = f . $1 );

consider n being Nat such that

A1: dom f = Seg n by FINSEQ_1:def 2;

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

consider F1 being Function such that

A2: rng F1 = Seg n and

A3: dom F1 in omega by FINSET_1:def 1;

ex b being object st S_{1}[a,b]

A6: ( dom F2 = dom f & ( for b being object st b in dom f holds

S_{1}[b,F2 . b] ) )
from CLASSES1:sch 1(A5);

set F = F2 * F1;

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

dom (F2 * F1) in omega by A6, A1, A2, A3, RELAT_1:27;

then { (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 ) } is finite by A14, FINSET_1:def 1;

then 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 ) } is finite by A4, FINSET_1:7;

hence still_not-bound_in f is finite by Th61; :: thesis: verum

let f be FinSequence of CQC-WFF Al; :: thesis: still_not-bound_in f is finite

defpred S

( $2 = still_not-bound_in p & p = f . $1 );

consider n being Nat such that

A1: dom f = Seg n by FINSEQ_1:def 2;

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

consider F1 being Function such that

A2: rng F1 = Seg n and

A3: dom F1 in omega by FINSET_1:def 1;

A4: now :: thesis: for b being set st b 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 ) } holds

b is finite

A5:
for a being object st a in dom f holds ( i in dom f & p = f . i ) } holds

b is finite

let b be set ; :: thesis: ( b 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 ) } implies b is finite )

assume b 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 ) } ; :: thesis: b is finite

then ex p being Element of CQC-WFF Al st

( b = still_not-bound_in p & ex i being Nat st

( i in dom f & p = f . i ) ) ;

hence b is finite by CQC_SIM1:19; :: thesis: verum

end;( i in dom f & p = f . i ) } implies b is finite )

assume b 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 ) } ; :: thesis: b is finite

then ex p being Element of CQC-WFF Al st

( b = still_not-bound_in p & ex i being Nat st

( i in dom f & p = f . i ) ) ;

hence b is finite by CQC_SIM1:19; :: thesis: verum

ex b being object st S

proof

consider F2 being Function such that
let a be object ; :: thesis: ( a in dom f implies ex b being object st S_{1}[a,b] )

assume a in dom f ; :: thesis: ex b being object st S_{1}[a,b]

then f . a in rng f by FUNCT_1:3;

then reconsider p = f . a as Element of CQC-WFF Al ;

take still_not-bound_in p ; :: thesis: S_{1}[a, still_not-bound_in p]

thus S_{1}[a, still_not-bound_in p]
; :: thesis: verum

end;assume a in dom f ; :: thesis: ex b being object st S

then f . a in rng f by FUNCT_1:3;

then reconsider p = f . a as Element of CQC-WFF Al ;

take still_not-bound_in p ; :: thesis: S

thus S

A6: ( dom F2 = dom f & ( for b being object st b in dom f holds

S

set F = F2 * F1;

A7: now :: thesis: for b being object st b 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 ) } holds

b in rng (F2 * F1)

( i in dom f & p = f . i ) } holds

b in rng (F2 * F1)

let b be object ; :: thesis: ( b 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 ) } implies b in rng (F2 * F1) )

assume b 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 ) } ; :: thesis: b in rng (F2 * F1)

then consider p being Element of CQC-WFF Al such that

A8: b = still_not-bound_in p and

A9: ex i being Nat st

( i in dom f & p = f . i ) ;

consider i being Nat such that

A10: i in dom f and

A11: p = f . i by A9;

S_{1}[i,F2 . i]
by A6, A10;

then b in rng F2 by A6, A8, A10, A11, FUNCT_1:3;

hence b in rng (F2 * F1) by A6, A1, A2, RELAT_1:28; :: thesis: verum

end;( i in dom f & p = f . i ) } implies b in rng (F2 * F1) )

assume b 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 ) } ; :: thesis: b in rng (F2 * F1)

then consider p being Element of CQC-WFF Al such that

A8: b = still_not-bound_in p and

A9: ex i being Nat st

( i in dom f & p = f . i ) ;

consider i being Nat such that

A10: i in dom f and

A11: p = f . i by A9;

S

then b in rng F2 by A6, A8, A10, A11, FUNCT_1:3;

hence b in rng (F2 * F1) by A6, A1, A2, RELAT_1:28; :: thesis: verum

now :: thesis: for b being object st b in rng (F2 * F1) holds

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

then A14:
rng (F2 * F1) = { (still_not-bound_in p) where p is Element of CQC-WFF Al : ex i being Nat st b 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 ) }

let b be object ; :: thesis: ( b in rng (F2 * F1) implies b 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 ) } )

assume b in rng (F2 * F1) ; :: thesis: b 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 ) }

then b in rng F2 by A6, A1, A2, RELAT_1:28;

then consider a being object such that

A12: a in dom F2 and

A13: b = F2 . a by FUNCT_1:def 3;

reconsider a = a as Element of NAT by A6, A12;

S_{1}[a,F2 . a]
by A6, A12;

hence b 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 A6, A12, A13; :: thesis: verum

end;( i in dom f & p = f . i ) } )

assume b in rng (F2 * F1) ; :: thesis: b 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 ) }

then b in rng F2 by A6, A1, A2, RELAT_1:28;

then consider a being object such that

A12: a in dom F2 and

A13: b = F2 . a by FUNCT_1:def 3;

reconsider a = a as Element of NAT by A6, A12;

S

hence b 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 A6, A12, A13; :: thesis: verum

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

dom (F2 * F1) in omega by A6, A1, A2, A3, RELAT_1:27;

then { (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 ) } is finite by A14, FINSET_1:def 1;

then 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 ) } is finite by A4, FINSET_1:7;

hence still_not-bound_in f is finite by Th61; :: thesis: verum