let n be Element of 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 & len p = height (tree w) )
by TREES_1:def 15;
A3:
( ( p = {} & len {} = 0 ) or ex n being Element of NAT ex q being FinSequence st
( n < len w & q in w . (n + 1) & p = <*n*> ^ q ) )
by A2, Def15;
now given k being
Element of
NAT ,
q being
FinSequence such that A4:
(
k < len w &
q in w . (k + 1) &
p = <*k*> ^ q )
;
:: thesis: height (tree w) <= n + 1A5:
(
w . (k + 1) in rng w &
rng w is
constituted-FinTrees )
by A4, Def10, Lm4;
then reconsider t =
w . (k + 1) as
finite Tree by Def4;
reconsider q =
q as
FinSequence of
NAT by A4, FINSEQ_1:50;
(
len q <= height t &
height t <= n &
len <*k*> = 1 )
by A1, A4, A5, FINSEQ_1:57, TREES_1:def 15;
then
(
len q <= n &
len p = 1
+ (len q) )
by A4, FINSEQ_1:35, XXREAL_0:2;
hence
height (tree w) <= n + 1
by A2, XREAL_1:9;
:: thesis: verum end;
hence
height (tree w) <= n + 1
by A2, A3; :: thesis: verum