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₁[ 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;

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

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;

A5: for a being object st a in dom f holds
ex b being object st S₁[a,b]

proof

let a be object ; :: thesis: ( a in dom f implies ex b being object st S₁[a,b] )
assume a in dom f ; :: thesis: ex b being object st S₁[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₁[a, still_not-bound_in p]
thus S₁[a, still_not-bound_in p] ; :: thesis: verum

end;

consider F2 being Function such that
A6: ( dom F2 = dom f & ( for b being object st b in dom f holds
S₁[b,F2 . b] ) ) from CLASSES1:sch 1(A5);
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)

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₁[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;

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

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₁[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;

then A14: rng (F2 * F1) = { (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 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