let t be DecoratedTree; :: thesis: for p, q being FinSequence of NAT st p ^ q in dom t holds
t | (p ^ q) = (t | p) | q
let p, q be FinSequence of NAT ; :: thesis: ( p ^ q in dom t implies t | (p ^ q) = (t | p) | q )
A1: dom (t | p) = (dom t) | p by TREES_2:def 10;
A2: dom (t | (p ^ q)) = (dom t) | (p ^ q) by TREES_2:def 10;
assume A3: p ^ q in dom t ; :: thesis: t | (p ^ q) = (t | p) | q
then A4: p in dom t by TREES_1:21;
then A5: q in (dom t) | p by A3, TREES_1:def 6;

A6: now :: thesis: for a being FinSequence of NAT st a in dom (t | (p ^ q)) holds
(t | (p ^ q)) . a = ((t | p) | q) . a

let a be FinSequence of NAT ; :: thesis: ( a in dom (t | (p ^ q)) implies (t | (p ^ q)) . a = ((t | p) | q) . a )
A7: (p ^ q) ^ a = p ^ (q ^ a) by FINSEQ_1:32;
assume A8: a in dom (t | (p ^ q)) ; :: thesis: (t | (p ^ q)) . a = ((t | p) | q) . a
then (p ^ q) ^ a in dom t by A3, A2, TREES_1:def 6;
then A9: q ^ a in (dom t) | p by A4, A7, TREES_1:def 6;
then A10: a in ((dom t) | p) | q by A5, TREES_1:def 6;
thus (t | (p ^ q)) . a = t . ((p ^ q) ^ a) by A2, A8, TREES_2:def 10
.= (t | p) . (q ^ a) by A7, A9, TREES_2:def 10
.= ((t | p) | q) . a by A1, A10, TREES_2:def 10 ; :: thesis: verum

end;

dom ((t | p) | q) = (dom (t | p)) | q by TREES_2:def 10;
hence t | (p ^ q) = (t | p) | q by A3, A1, A2, A6, Th2; :: thesis: verum