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