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