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