let T be Tree; :: thesis: for p being FinSequence holds
( p in T iff <*0 *> ^ p in ^ T )
let p be FinSequence; :: thesis: ( p in T iff <*0 *> ^ p in ^ T )
thus ( p in T implies <*0 *> ^ p in ^ T ) by Th63; :: thesis: ( <*0 *> ^ p in ^ T implies p in T )
assume <*0 *> ^ p in ^ T ; :: thesis: p in T
then consider n being Element of NAT , q being FinSequence such that
A1: ( n < len <*T*> & q in <*T*> . (n + 1) & <*0 *> ^ p = <*n*> ^ q ) by Def15;
( (<*0 *> ^ p) . 1 = 0 & (<*n*> ^ q) . 1 = n ) by FINSEQ_1:58;
then ( p = q & <*T*> . (n + 1) = T ) by A1, FINSEQ_1:46, FINSEQ_1:57;
hence p in T by A1; :: thesis: verum