let n be Nat; for w being FinTree-yielding FinSequence st ( for t being finite Tree st t in rng w holds
height t <= n ) holds
height (tree w) <= n + 1
let w be FinTree-yielding FinSequence; ( ( for t being finite Tree st t in rng w holds
height t <= n ) implies height (tree w) <= n + 1 )
assume A1:
for t being finite Tree st t in rng w holds
height t <= n
; height (tree w) <= n + 1
consider p being FinSequence of NAT such that
A2:
p in tree w
and
A3:
len p = height (tree w)
by TREES_1:def 12;
A4:
( ( p = {} & len {} = 0 ) or ex n being Nat ex q being FinSequence st
( n < len w & q in w . (n + 1) & p = <*n*> ^ q ) )
by A2, Def15;
now ( ex k being Nat ex q being FinSequence st
( k < len w & q in w . (k + 1) & p = <*k*> ^ q ) implies height (tree w) <= n + 1 )given k being
Nat,
q being
FinSequence such that A5:
k < len w
and A6:
q in w . (k + 1)
and A7:
p = <*k*> ^ q
;
height (tree w) <= n + 1A8:
w . (k + 1) in rng w
by A5, Lm3;
rng w is
constituted-FinTrees
by Def10;
then reconsider t =
w . (k + 1) as
finite Tree by A8;
reconsider q =
q as
FinSequence of
NAT by A7, FINSEQ_1:36;
A9:
len q <= height t
by A6, TREES_1:def 12;
A10:
height t <= n
by A1, A5, Lm3;
A11:
len <*k*> = 1
by FINSEQ_1:40;
A12:
len q <= n
by A9, A10, XXREAL_0:2;
len p = 1
+ (len q)
by A7, A11, FINSEQ_1:22;
hence
height (tree w) <= n + 1
by A3, A12, XREAL_1:7;
verum end;
hence
height (tree w) <= n + 1
by A3, A4; verum