let n be Nat; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: 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 :: thesis: ( 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 ; :: thesis: height (tree w) <= n + 1
A8: 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; :: thesis: verum

end;

hence height (tree w) <= n + 1 by A3, A4; :: thesis: verum