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