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:] by RELAT_1:def 19;
then A4: dom (T `1 ) = dom T by A1, RELAT_1:46;
A5: dom (T `2 ) = dom T by A2, A3, RELAT_1:46;
then A6: dom <:(T `1 ),(T `2 ):> = dom T by A4, FUNCT_3:70;

now

let x be set ; :: 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:69
.= [((T . t) `1 ),((T `2 ) . t)] by Th41
.= [((T . t) `1 ),((T . t) `2 )] by Th41
.= T . x by MCART_1:23 ; :: thesis: verum

end;

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