let D1, D2 be non empty set ; 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; 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; ( (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; verum