A0: <*> NAT in dom d1 by TREES_1:22;
then A1: dom (d1 with-replacement ((<*> NAT),d)) = (dom d1) with-replacement ((<*> NAT),(dom d)) by TREES_2:def 11;
hence dom (d1 with-replacement ((<*> NAT),d)) = dom d ; :: according to TREES_4:def 1 :: thesis: for b₁ being Element of proj1 (d1 with-replacement ((<*> NAT),d)) holds (d1 with-replacement ((<*> NAT),d)) . b₁ = d . b₁
let p be Element of dom (d1 with-replacement ((<*> NAT),d)); :: thesis: (d1 with-replacement ((<*> NAT),d)) . p = d . p
( ( not {} is_a_prefix_of p & (d1 with-replacement ((<*> NAT),d)) . p = d1 . p ) or ex r being FinSequence of NAT st
( r in dom d & p = {} ^ r & (d1 with-replacement ((<*> NAT),d)) . p = d . r ) ) by A0, A1, TREES_2:def 11;
hence (d1 with-replacement ((<*> NAT),d)) . p = d . p ; :: thesis: verum