let x be set ; :: thesis: ( x -flat_tree {} = root-tree x & x -tree {} = root-tree x )
A1: len {} = 0 ;
A2: dom (x -flat_tree {} ) = elementary_tree 0 by A1, Def3;

A3: now

let y be set ; :: thesis: ( y in elementary_tree 0 implies (x -flat_tree {} ) . y = x )
assume A4: y in elementary_tree 0 ; :: thesis: (x -flat_tree {} ) . y = x
A5: y = {} by A4, TARSKI:def 1, TREES_1:56;
thus (x -flat_tree {} ) . y = x by A5, Def3; :: thesis: verum

end;

thus x -flat_tree {} = root-tree x by A2, A3, FUNCOP_1:17; :: thesis: x -tree {} = root-tree x
reconsider e = {} as DTree-yielding FinSequence ;
A6: dom (x -tree {} ) = tree (doms e) by Th10
.= elementary_tree 0 by FUNCT_6:32, TREES_3:55 ;

A7: now

let y be set ; :: thesis: ( y in elementary_tree 0 implies (x -tree e) . y = x )
assume A8: y in elementary_tree 0 ; :: thesis: (x -tree e) . y = x
A9: y = {} by A8, TARSKI:def 1, TREES_1:56;
thus (x -tree e) . y = x by A9, Def4; :: thesis: verum

end;

thus x -tree {} = root-tree x by A6, A7, FUNCOP_1:17; :: thesis: verum