set a = union (Subt (rng P));
{} in dom T
by TREES_1:22;
hence
not rng T is empty
by FUNCT_1:3; rng T is finite
rng T c= [:((union (Subt (rng P))) **),((union (Subt (rng P))) **):]
proof
let x be
object ;
TARSKI:def 3 ( not x in rng T or x in [:((union (Subt (rng P))) **),((union (Subt (rng P))) **):] )
assume A1:
x in rng T
;
x in [:((union (Subt (rng P))) **),((union (Subt (rng P))) **):]
then reconsider x1 =
x as
PNPair ;
A2:
rng x1 c= union (Subt (rng P))
by Th27, A1;
rng (x1 `1) c= rng x1
by XBOOLE_1:7;
then
x1 `1 is
one-to-one FinSequence of
union (Subt (rng P))
by XBOOLE_1:1, A2, FINSEQ_1:def 4;
then A3:
x1 `1 in (union (Subt (rng P))) **
by LTLAXIO3:def 2;
rng (x1 `2) c= rng x1
by XBOOLE_1:7;
then
x1 `2 is
one-to-one FinSequence of
union (Subt (rng P))
by XBOOLE_1:1, A2, FINSEQ_1:def 4;
then A4:
x1 `2 in (union (Subt (rng P))) **
by LTLAXIO3:def 2;
consider y,
z being
object such that A5:
(
y in LTLB_WFF ** &
z in LTLB_WFF ** )
and A6:
x1 = [y,z]
by ZFMISC_1:def 2;
reconsider y =
y,
z =
z as
one-to-one FinSequence of
LTLB_WFF by A5, LTLAXIO3:def 2;
thus
x in [:((union (Subt (rng P))) **),((union (Subt (rng P))) **):]
by A3, A4, ZFMISC_1:def 2, A6;
verum
end;
hence
rng T is finite
; verum