let w be FinTree-yielding FinSequence; :: thesis: for t being finite Tree st t in rng w holds
height (tree w) > height t
let t be finite Tree; :: thesis: ( t in rng w implies height (tree w) > height t )
assume t in rng w ; :: thesis: height (tree w) > height t
then consider x being set such that
A1: ( x in dom w & t = w . x ) by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A1;
A2: ( 1 <= x & len w >= x ) by A1, FINSEQ_3:27;
then consider n being Nat such that
A3: x = 1 + n by NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
( n < len w & {} in t & <*n*> ^ {} = <*n*> ) by A2, A3, FINSEQ_1:47, NAT_1:13, TREES_1:47;
then ( t = (tree w) | <*n*> & <*n*> in tree w & <*n*> <> {} ) by A1, A3, Def15, Th52;
hence height (tree w) > height t by TREES_1:85; :: thesis: verum