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:40;
<*T1,T2*> = <*T1,T2*> ^ {} by FINSEQ_1:34;
hence for p being FinSequence holds
( p in T2 iff <*1*> ^ p in tree (T1,T2) ) by A1, A2, Th51; :: thesis: verum