let D1, D2 be non empty set ; 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; ( 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; verum