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