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