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:61;
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:61 ; :: 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:61 ; :: thesis: verum