set a = union (Subt (rng P));
{} in dom T by TREES_1:22;
hence not rng T is empty by FUNCT_1:3; :: thesis: rng T is finite
rng T c= [:((union (Subt (rng P))) **),((union (Subt (rng P))) **):]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng T or x in [:((union (Subt (rng P))) **),((union (Subt (rng P))) **):] )
assume A1: x in rng T ; :: thesis: 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; :: thesis: verum

end;

hence rng T is finite ; :: thesis: verum