let D1, D2 be non empty set ; :: thesis: for T being DecoratedTree of D1,D2 holds

( dom (T `1) = dom T & dom (T `2) = dom T )

let T be DecoratedTree of D1,D2; :: thesis: ( dom (T `1) = dom T & dom (T `2) = dom T )

A1: ( T `1 = (pr1 (D1,D2)) * T & T `2 = (pr2 (D1,D2)) * T ) by TREES_3:def 12, TREES_3:def 13;

A2: ( rng T c= [:D1,D2:] & dom (pr1 (D1,D2)) = [:D1,D2:] ) by FUNCT_2:def 1, RELAT_1:def 19;

dom (pr2 (D1,D2)) = [:D1,D2:] by FUNCT_2:def 1;

hence ( dom (T `1) = dom T & dom (T `2) = dom T ) by A1, A2, RELAT_1:27; :: thesis: verum

( dom (T `1) = dom T & dom (T `2) = dom T )

let T be DecoratedTree of D1,D2; :: thesis: ( dom (T `1) = dom T & dom (T `2) = dom T )

A1: ( T `1 = (pr1 (D1,D2)) * T & T `2 = (pr2 (D1,D2)) * T ) by TREES_3:def 12, TREES_3:def 13;

A2: ( rng T c= [:D1,D2:] & dom (pr1 (D1,D2)) = [:D1,D2:] ) by FUNCT_2:def 1, RELAT_1:def 19;

dom (pr2 (D1,D2)) = [:D1,D2:] by FUNCT_2:def 1;

hence ( dom (T `1) = dom T & dom (T `2) = dom T ) by A1, A2, RELAT_1:27; :: thesis: verum