let D1, D2 be non empty set ; :: thesis: for T being DecoratedTree of , holds
( dom (T `1 ) = dom T & dom (T `2 ) = dom T )
let T be DecoratedTree of ,; :: thesis: ( dom (T `1 ) = dom T & dom (T `2 ) = dom T )
( T `1 = (pr1 D1,D2) * T & T `2 = (pr2 D1,D2) * T & rng T c= [:D1,D2:] & dom (pr1 D1,D2) = [:D1,D2:] & dom (pr2 D1,D2) = [:D1,D2:] ) by FUNCT_2:def 1, RELAT_1:def 19, TREES_3:def 12, TREES_3:def 13;
hence ( dom (T `1 ) = dom T & dom (T `2 ) = dom T ) by RELAT_1:46; :: thesis: verum