let D1, D2 be non empty set ; for T being DecoratedTree of D1,D2 holds <:(T `1),(T `2):> = T
let T be DecoratedTree of D1,D2; <:(T `1),(T `2):> = T
A1:
dom (pr1 (D1,D2)) = [:D1,D2:]
by FUNCT_2:def 1;
A2:
dom (pr2 (D1,D2)) = [:D1,D2:]
by FUNCT_2:def 1;
A3:
rng T c= [:D1,D2:]
;
then A4:
dom (T `1) = dom T
by A1, RELAT_1:27;
A5:
dom (T `2) = dom T
by A2, A3, RELAT_1:27;
then A6:
dom <:(T `1),(T `2):> = dom T
by A4, FUNCT_3:50;
hence
<:(T `1),(T `2):> = T
by A6; verum