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
n < len <*T*> and
A1: q in <*T*> . (n + 1) and
A2: <*0 *> ^ p = <*n*> ^ q by Def15;
A3: (<*0 *> ^ p) . 1 = 0 by FINSEQ_1:58;
A4: (<*n*> ^ q) . 1 = n by FINSEQ_1:58;
then p = q by A2, A3, FINSEQ_1:46;
hence p in T by A1, A2, A3, A4, FINSEQ_1:57; :: thesis: verum