let X be non empty set ; :: thesis: for p being FinSequence of FinTrees X
for x, t being set st t in rng p holds
t <> x -tree p
let p be FinSequence of FinTrees X; :: thesis: for x, t being set st t in rng p holds
t <> x -tree p
let x, t be set ; :: thesis: ( t in rng p implies t <> x -tree p )
assume A1: t in rng p ; :: thesis: t <> x -tree p
then reconsider T = t as Element of FinTrees X ;
reconsider A = dom T as finite Tree ;
defpred S₁[ set ] means verum;
deffunc H₁( Element of A) -> Element of omega = len $1;
{ H₁(e) where e is Element of A : S₁[e] } is finite from PRE_CIRC:sch 1();
then reconsider B = { H₁(e) where e is Element of A : S₁[e] } as finite set ;
set e = the Element of A;
A2: H₁( the Element of A) in B ;
B is real-membered

proof

let a be object ; :: according to MEMBERED:def 3 :: thesis: ( a nin B or not a is real )
assume a in B ; :: thesis: a is real
then ex e being Element of A st a = H₁(e) ;
hence a is real ; :: thesis: verum

end;

then reconsider B = B as non empty finite real-membered set by A2;
max B in B by XXREAL_2:def 8;
then consider e being Element of A such that
A3: max B = len e ;
consider i being object such that
A4: i in dom p and
A5: t = p . i by A1, FUNCT_1:def 3;
reconsider i = i as Nat by A4;
i >= 1 by A4, FINSEQ_3:25;
then consider j being Nat such that
A6: i = 1 + j by NAT_1:10;
i <= len p by A4, FINSEQ_3:25;
then A7: j < len p by A6, NAT_1:13;
A8: <*j*> ^ e in dom (x -tree p) by A5, A6, A7, TREES_4:11;
len (<*j*> ^ e) = 1 + (len e) by FINSEQ_5:8;
then len (<*j*> ^ e) > max B by A3, NAT_1:13;
then len (<*j*> ^ e) nin B by XXREAL_2:def 8;
hence t <> x -tree p by A8; :: thesis: verum