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;
now :: thesis: for y being object st y in elementary_tree 0 holds
(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;
hence x -flat_tree {} = root-tree x by A1; :: thesis: x -tree {} = root-tree x
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
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;
hence x -tree {} = root-tree x by A2; :: thesis: verum