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