let T be finite Tree; :: thesis: height (^ T) = (height T) + 1
set m = height T;
A1: rng <*T*> = {T} by FINSEQ_1:38;
A2: T in {T} by TARSKI:def 1;
for t being finite Tree st t in rng <*T*> holds
height t <= height T by A1, TARSKI:def 1;
hence height (^ T) = (height T) + 1 by A1, A2, Th79; :: thesis: verum