let x be object ; :: thesis: ( x -flat_tree {} = root-tree x & x -tree {} = root-tree x )

len {} = 0 ;

then A1: dom (x -flat_tree {}) = elementary_tree 0 by Def3;

reconsider e = {} as DTree-yielding FinSequence ;

A2: dom (x -tree {}) = tree (doms e) by Th10

.= elementary_tree 0 by FUNCT_6:23, TREES_3:52 ;

len {} = 0 ;

then A1: dom (x -flat_tree {}) = elementary_tree 0 by Def3;

now :: thesis: for y being object st y in elementary_tree 0 holds

(x -flat_tree {}) . y = x

hence
x -flat_tree {} = root-tree x
by A1; :: thesis: x -tree {} = root-tree x(x -flat_tree {}) . y = x

let y be object ; :: thesis: ( y in elementary_tree 0 implies (x -flat_tree {}) . y = x )

assume y in elementary_tree 0 ; :: thesis: (x -flat_tree {}) . y = x

then y = {} by TARSKI:def 1, TREES_1:29;

hence (x -flat_tree {}) . y = x by Def3; :: thesis: verum

end;assume y in elementary_tree 0 ; :: thesis: (x -flat_tree {}) . y = x

then y = {} by TARSKI:def 1, TREES_1:29;

hence (x -flat_tree {}) . y = x by Def3; :: thesis: verum

reconsider e = {} as DTree-yielding FinSequence ;

A2: dom (x -tree {}) = tree (doms e) by Th10

.= elementary_tree 0 by FUNCT_6:23, TREES_3:52 ;

now :: thesis: for y being object st y in elementary_tree 0 holds

(x -tree e) . y = x

hence
x -tree {} = root-tree x
by A2; :: thesis: verum(x -tree e) . y = x

let y be object ; :: thesis: ( y in elementary_tree 0 implies (x -tree e) . y = x )

assume y in elementary_tree 0 ; :: thesis: (x -tree e) . y = x

then y = {} by TARSKI:def 1, TREES_1:29;

hence (x -tree e) . y = x by Def4; :: thesis: verum

end;assume y in elementary_tree 0 ; :: thesis: (x -tree e) . y = x

then y = {} by TARSKI:def 1, TREES_1:29;

hence (x -tree e) . y = x by Def4; :: thesis: verum