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 object such that
A1: x in dom w and
A2: t = w . x by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A1;
A3: 1 <= x by A1, FINSEQ_3:25;
A4: len w >= x by A1, FINSEQ_3:25;
consider n being Nat such that
A5: x = 1 + n by A3, NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A6: n < len w by A4, A5, NAT_1:13;
A7: {} in t by TREES_1:22;
A8: <*n*> ^ {} = <*n*> by FINSEQ_1:34;
A9: t = (tree w) | <*n*> by A2, A5, A6, Th49;
<*n*> in tree w by A2, A5, A6, A7, A8, Def15;
hence height (tree w) > height t by A9, TREES_1:48; :: thesis: verum