let T1, T2 be Tree; :: thesis: ( (tree (T1,T2)) | <*0*> = T1 & (tree (T1,T2)) | <*1*> = T2 )
set p = <*T1,T2*>;
A1: len <*T1,T2*> = 2 by FINSEQ_1:44;
A2: <*T1,T2*> . 1 = T1 ;
A3: <*T1,T2*> . 2 = T2 ;
A4: 0 + 1 = 1 ;
1 + 1 = 2 ;
hence ( (tree (T1,T2)) | <*0*> = T1 & (tree (T1,T2)) | <*1*> = T2 ) by A1, A2, A3, A4, Th49; :: thesis: verum