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) by FINSEQ_1:22;
A2: len (p1 ^ <*T*>) = (len p1) + (len <*T*>) by FINSEQ_1:22;
A3: len <*T*> = 1 by FINSEQ_1:40;
A4: ((len p1) + 1) + (len p2) = ((len p1) + (len p2)) + 1 ;
len p1 <= (len p1) + (len p2) by NAT_1:11;
then A5: len p1 < len ((p1 ^ <*T*>) ^ p2) by A1, A2, A3, A4, NAT_1:13;
(len p1) + 1 >= 1 by NAT_1:11;
then (len p1) + 1 in dom (p1 ^ <*T*>) by A2, A3, FINSEQ_3:25;
then A6: ((p1 ^ <*T*>) ^ p2) . ((len p1) + 1) = (p1 ^ <*T*>) . ((len p1) + 1) by FINSEQ_1:def 7
.= T by FINSEQ_1:42 ;
hence ( p in T implies <*(len p1)*> ^ p in tree ((p1 ^ <*T*>) ^ p2) ) by A5, 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 Nat, q being FinSequence such that
n < len ((p1 ^ <*T*>) ^ p2) and
A7: q in ((p1 ^ <*T*>) ^ p2) . (n + 1) and
A8: <*(len p1)*> ^ p = <*n*> ^ q by Def15;
A9: (<*(len p1)*> ^ p) . 1 = len p1 by FINSEQ_1:41;
(<*n*> ^ q) . 1 = n by FINSEQ_1:41;
hence p in T by A6, A7, A8, A9, FINSEQ_1:33; :: thesis: verum