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 Th60; :: thesis: ( <*0*> ^ p in ^ T implies p in T )
assume <*0*> ^ p in ^ T ; :: thesis: p in T
then consider n being 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:41;
A4: (<*n*> ^ q) . 1 = n by FINSEQ_1:41;
then p = q by A2, A3, FINSEQ_1:33;
hence p in T by A1, A2, A3, A4; :: thesis: verum