let x be set ; :: thesis: for T1, T2 being DecoratedTree holds
( (x -tree (T1,T2)) | <*0*> = T1 & (x -tree (T1,T2)) | <*1*> = T2 )
let T1, T2 be DecoratedTree; :: thesis: ( (x -tree (T1,T2)) | <*0*> = T1 & (x -tree (T1,T2)) | <*1*> = T2 )
A1: len <*T1,T2*> = 2 by FINSEQ_1:44;
thus (x -tree (T1,T2)) | <*0*> = (x -tree <*T1,T2*>) | <*0*> by TREES_4:def 6
.= <*T1,T2*> . (0 + 1) by A1, TREES_4:def 4
.= T1 by FINSEQ_1:44 ; :: thesis: (x -tree (T1,T2)) | <*1*> = T2
thus (x -tree (T1,T2)) | <*1*> = (x -tree <*T1,T2*>) | <*1*> by TREES_4:def 6
.= <*T1,T2*> . (1 + 1) by A1, TREES_4:def 4
.= T2 by FINSEQ_1:44 ; :: thesis: verum