let x, y be object ; :: 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) by Def3;
hence p = {} by A1, Th2; :: thesis: verum