let T be Tree; :: thesis: (^ T) | <*0 *> = T
set p = <*T*>;
( len <*T*> = 1 & <*T*> . 1 = T & 0 + 1 = 1 & 0 < 1 & ^ T = tree <*T*> ) by FINSEQ_1:57;
hence (^ T) | <*0 *> = T by Th52; :: thesis: verum