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