A1:
dom (doms p) = dom p
by TREES_3:37;

A2: rng p c= FinTrees D by FINSEQ_1:def 4;

thus doms p is FinSequence of FinTrees :: thesis: verum

A2: rng p c= FinTrees D by FINSEQ_1:def 4;

thus doms p is FinSequence of FinTrees :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis: ( not x in rng (doms p) or x in FinTrees )

assume x in rng (doms p) ; :: thesis: x in FinTrees

then consider y being object such that

A3: y in dom p and

A4: x = (doms p) . y by A1, FUNCT_1:def 3;

reconsider T = p . y as DecoratedTree by A3, TREES_3:24;

T in rng p by A3, FUNCT_1:def 3;

then dom T in FinTrees by A2, TREES_3:def 2;

hence x in FinTrees by A3, A4, FUNCT_6:22; :: thesis: verum

end;assume x in rng (doms p) ; :: thesis: x in FinTrees

then consider y being object such that

A3: y in dom p and

A4: x = (doms p) . y by A1, FUNCT_1:def 3;

reconsider T = p . y as DecoratedTree by A3, TREES_3:24;

T in rng p by A3, FUNCT_1:def 3;

then dom T in FinTrees by A2, TREES_3:def 2;

hence x in FinTrees by A3, A4, FUNCT_6:22; :: thesis: verum