let p be FinSequence; :: thesis: for p1, p2 being Tree-yielding FinSequence
for T being Tree holds
( p in T iff <*(len p1)*> ^ p in tree ((p1 ^ <*T*>) ^ p2) )
let p1, p2 be Tree-yielding FinSequence; :: thesis: for T being Tree holds
( p in T iff <*(len p1)*> ^ p in tree ((p1 ^ <*T*>) ^ p2) )
let T be Tree; :: thesis: ( p in T iff <*(len p1)*> ^ p in tree ((p1 ^ <*T*>) ^ p2) )
A1: ( len ((p1 ^ <*T*>) ^ p2) = (len (p1 ^ <*T*>)) + (len p2) & len (p1 ^ <*T*>) = (len p1) + (len <*T*>) & len <*T*> = 1 ) by FINSEQ_1:35, FINSEQ_1:57;
((len p1) + 1) + (len p2) = ((len p1) + (len p2)) + 1 ;
then ( (len p1) + (len p2) < len ((p1 ^ <*T*>) ^ p2) & len p1 <= (len p1) + (len p2) ) by A1, NAT_1:11, NAT_1:13;
then A2: len p1 < len ((p1 ^ <*T*>) ^ p2) by XXREAL_0:2;
(len p1) + 1 >= 1 by NAT_1:11;
then (len p1) + 1 in dom (p1 ^ <*T*>) by A1, FINSEQ_3:27;
then A3: ((p1 ^ <*T*>) ^ p2) . ((len p1) + 1) = (p1 ^ <*T*>) . ((len p1) + 1) by FINSEQ_1:def 7
.= T by FINSEQ_1:59 ;
hence ( p in T implies <*(len p1)*> ^ p in tree ((p1 ^ <*T*>) ^ p2) ) by A2, Def15; :: thesis: ( <*(len p1)*> ^ p in tree ((p1 ^ <*T*>) ^ p2) implies p in T )
assume <*(len p1)*> ^ p in tree ((p1 ^ <*T*>) ^ p2) ; :: thesis: p in T
then consider n being Element of NAT , q being FinSequence such that
A4: ( n < len ((p1 ^ <*T*>) ^ p2) & q in ((p1 ^ <*T*>) ^ p2) . (n + 1) & <*(len p1)*> ^ p = <*n*> ^ q ) by Def15;
( (<*(len p1)*> ^ p) . 1 = len p1 & (<*n*> ^ q) . 1 = n ) by FINSEQ_1:58;
hence p in T by A3, A4, FINSEQ_1:46; :: thesis: verum