let x be set ; for T1, T2 being DecoratedTree holds
( (x -tree (T1,T2)) | <*0*> = T1 & (x -tree (T1,T2)) | <*1*> = T2 )
let T1, T2 be DecoratedTree; ( (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
; (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
; verum