let x, y be set ; :: thesis: for p being FinSequence st root-tree x = y -flat_tree p holds
( x = y & p = {} )
let p be FinSequence; :: thesis: ( root-tree x = y -flat_tree p implies ( x = y & p = {} ) )
assume A1: root-tree x = y -flat_tree p ; :: thesis: ( x = y & p = {} )
thus x = (root-tree x) . {} by Th3
.= y by A1, Def3 ; :: thesis: p = {}
( dom (y -flat_tree p) = elementary_tree (len p) & dom (root-tree x) = elementary_tree 0 ) by Def3, Th3;
then len p = 0 by A1, Th2;
hence p = {} ; :: thesis: verum