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:] ;
then A4: dom (T `1) = dom T by A1, RELAT_1:27;
A5: dom (T `2) = dom T by A2, A3, RELAT_1:27;
A6: T . t = [((T . t) `1),((T . t) `2)] by MCART_1:21;
then A7: (T `1) . t = (pr1 (D1,D2)) . (((T . t) `1),((T . t) `2)) by A4, FUNCT_1:12;
(T `2) . t = (pr2 (D1,D2)) . (((T . t) `1),((T . t) `2)) by A5, A6, FUNCT_1:12;
hence ( (T . t) `1 = (T `1) . t & (T `2) . t = (T . t) `2 ) by A7, FUNCT_3:def 4, FUNCT_3:def 5; :: thesis: verum