let D1, D2 be non empty set ; :: thesis: for T being DecoratedTree of D1,D2
for t being Element of dom T holds
( (T . t) `1 = (T `1 ) . t & (T `2 ) . t = (T . t) `2 )
let T be DecoratedTree of D1,D2; :: thesis: for t being Element of dom T holds
( (T . t) `1 = (T `1 ) . t & (T `2 ) . t = (T . t) `2 )
let t be Element of dom T; :: thesis: ( (T . t) `1 = (T `1 ) . t & (T `2 ) . t = (T . t) `2 )
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;
A6: T . t = [((T . t) `1 ),((T . t) `2 )] by MCART_1:23;
then A7: (T `1 ) . t = (pr1 D1,D2) . ((T . t) `1 ),((T . t) `2 ) by A4, FUNCT_1:22;
(T `2 ) . t = (pr2 D1,D2) . ((T . t) `1 ),((T . t) `2 ) by A5, A6, FUNCT_1:22;
hence ( (T . t) `1 = (T `1 ) . t & (T `2 ) . t = (T . t) `2 ) by A7, FUNCT_3:def 5, FUNCT_3:def 6; :: thesis: verum