let x be set ; :: thesis: for T being DecoratedTree holds dom (x -tree T) = ^ (dom T)
let T be DecoratedTree; :: thesis: dom (x -tree T) = ^ (dom T)
A1: ( dom (x -tree <*T*>) = tree (doms <*T*>) & doms <*T*> = <*(dom T)*> ) by Th10, FUNCT_6:33;
thus dom (x -tree T) = ^ (dom T) by A1, TREES_3:def 16; :: thesis: verum