let D1, D2 be non empty set ; :: thesis: for T being DecoratedTree of ,
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 ,; :: 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 )
( T `1 = (pr1 D1,D2) * T & T `2 = (pr2 D1,D2) * T & dom (pr1 D1,D2) = [:D1,D2:] & dom (pr2 D1,D2) = [:D1,D2:] & rng T c= [:D1,D2:] ) by FUNCT_2:def 1, RELAT_1:def 19;
then A1: ( dom (T `1 ) = dom T & dom (T `2 ) = dom T ) by RELAT_1:46;
T . t = [((T . t) `1 ),((T . t) `2 )] by MCART_1:23;
then ( (T `1 ) . t = (pr1 D1,D2) . ((T . t) `1 ),((T . t) `2 ) & (T `2 ) . t = (pr2 D1,D2) . ((T . t) `1 ),((T . t) `2 ) ) by A1, FUNCT_1:22;
hence ( (T . t) `1 = (T `1 ) . t & (T `2 ) . t = (T . t) `2 ) by FUNCT_3:def 5, FUNCT_3:def 6; :: thesis: verum