let D1, D2 be non empty set ; :: thesis: for T being DecoratedTree of D1,D2 holds <:(T `1),(T `2):> = T
let T be DecoratedTree of D1,D2; :: thesis: <:(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;

now :: thesis: for x being object st x in dom T holds
<:(T `1),(T `2):> . x = T . x

let x be object ; :: thesis: ( x in dom T implies <:(T `1),(T `2):> . x = T . x )
assume x in dom T ; :: thesis: <:(T `1),(T `2):> . x = T . x
then reconsider t = x as Element of dom T ;
thus <:(T `1),(T `2):> . x = [((T `1) . t),((T `2) . t)] by A4, A5, FUNCT_3:49
.= [((T . t) `1),((T `2) . t)] by Th39
.= [((T . t) `1),((T . t) `2)] by Th39
.= T . x by MCART_1:21 ; :: thesis: verum

end;

hence <:(T `1),(T `2):> = T by A6; :: thesis: verum