let T1, T2 be Tree; :: thesis: for p being FinSequence holds
( p in T1 iff <*0 *> ^ p in tree T1,T2 )
( tree T1,T2 = tree <*T1,T2*> & <*T1,T2*> = <*T1*> ^ <*T2*> & <*T1*> = {} ^ <*T1*> & len {} = 0 ) by FINSEQ_1:47, FINSEQ_1:def 9;
hence for p being FinSequence holds
( p in T1 iff <*0 *> ^ p in tree T1,T2 ) by Th54; :: thesis: verum