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;
A2: <*T1,T2*> . (0 + 1) = T1 by FINSEQ_1:61;
reconsider w = {} as Node of T1 by TREES_1:47;
thus (x -tree T1,T2) . <*0 *> = (x -tree <*T1,T2*>) . <*0 *> by TREES_4:def 6
.= (x -tree <*T1,T2*>) . (<*0 *> ^ w) by FINSEQ_1:47
.= T1 . {} by A1, A2, TREES_4:12 ; :: thesis: (x -tree T1,T2) . <*1*> = T2 . {}
A3: <*T1,T2*> . (1 + 1) = T2 by FINSEQ_1:61;
reconsider w = {} as Node of T2 by TREES_1:47;
thus (x -tree T1,T2) . <*1*> = (x -tree <*T1,T2*>) . <*1*> by TREES_4:def 6
.= (x -tree <*T1,T2*>) . (<*1*> ^ w) by FINSEQ_1:47
.= T2 . {} by A1, A3, TREES_4:12 ; :: thesis: verum