let T be Tree; :: thesis: for x being object holds
( x in ^ T iff ( x = {} or ex p being FinSequence st
( p in T & x = <*0*> ^ p ) ) )
let x be object ; :: thesis: ( x in ^ T iff ( x = {} or ex p being FinSequence st
( p in T & x = <*0*> ^ p ) ) )
set p = <*T*>;
A1: len <*T*> = 1 by FINSEQ_1:40;
A2: <*T*> . 1 = T ;
thus ( x in ^ T & x <> {} implies ex p being FinSequence st
( p in T & x = <*0*> ^ p ) ) :: thesis: ( ( x = {} or ex p being FinSequence st
( p in T & x = <*0*> ^ p ) ) implies x in ^ T )

proof

assume that
A3: x in ^ T and
A4: x <> {} ; :: thesis: ex p being FinSequence st
( p in T & x = <*0*> ^ p )
consider n being Nat, q being FinSequence such that
A5: n < len <*T*> and
A6: q in <*T*> . (n + 1) and
A7: x = <*n*> ^ q by A3, A4, Def15;
0 + 1 = 1 ;
then n = 0 by A1, A5, NAT_1:13;
hence ex p being FinSequence st
( p in T & x = <*0*> ^ p ) by A6, A7; :: thesis: verum

end;

0 < 0 + 1 ;
hence ( ( x = {} or ex p being FinSequence st
( p in T & x = <*0*> ^ p ) ) implies x in ^ T ) by A1, A2, Def15; :: thesis: verum