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:61;
A2: <*T1,T2*> . 1 = T1 by FINSEQ_1:61;
A3: <*T1,T2*> . 2 = T2 by FINSEQ_1:61;
A4: 0 + 1 = 1 ;
1 + 1 = 2 ;
hence ( (tree T1,T2) | <*0 *> = T1 & (tree T1,T2) | <*1*> = T2 ) by A1, A2, A3, A4, Th52; :: thesis: verum