let t be DecoratedTree; 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 ; ( 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
; 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 for a being FinSequence of NAT st a in dom (t | (p ^ q)) holds
(t | (p ^ q)) . a = ((t | p) | q) . alet a be
FinSequence of
NAT ;
( 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))
;
(t | (p ^ q)) . a = ((t | p) | q) . athen
(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
;
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; verum