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:
defpred S1[ 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 = { 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 { 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 { 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 { 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 S1[a,b]
proof
let a be object ; :: thesis: ( a in dom f implies ex b being object st S1[a,b] )
assume a in dom f ; :: thesis: ex b being object st S1[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: S1[a, still_not-bound_in p]
thus S1[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
S1[b,F2 . b] ) ) from set F = F2 * F1;
A7: now :: thesis: for b being object st b in { 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 { 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 { 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;
S1[i,F2 . i] by ;
then b in rng F2 by ;
hence b in rng (F2 * F1) by ; :: thesis: verum
end;
now :: thesis: for b being object st b in rng (F2 * F1) holds
b in { 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 { 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 { 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 ;
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 ;
S1[a,F2 . a] by ;
hence b in { 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) = { where p is Element of CQC-WFF Al : ex i being Nat st
( i in dom f & p = f . i )
}
by ;
dom (F2 * F1) in omega by ;
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 ;
then union { where p is Element of CQC-WFF Al : ex i being Nat st
( i in dom f & p = f . i )
}
is finite by ;
hence still_not-bound_in f is finite by Th61; :: thesis: verum