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 )
assume A1:
p ^ q in dom t
; :: thesis: t | (p ^ q) = (t | p) | q
then A2:
( (dom t) | (p ^ q) = ((dom t) | p) | q & p in dom t )
by Th2, TREES_1:46;
then A3:
q in (dom t) | p
by A1, TREES_1:def 9;
A4:
( dom (t | p) = (dom t) | p & dom (t | (p ^ q)) = (dom t) | (p ^ q) & dom ((t | p) | q) = (dom (t | p)) | q )
by TREES_2:def 11;
now let a be
FinSequence of
NAT ;
:: thesis: ( a in dom (t | (p ^ q)) implies (t | (p ^ q)) . a = ((t | p) | q) . a )A5:
(p ^ q) ^ a = p ^ (q ^ a)
by FINSEQ_1:45;
assume A6:
a in dom (t | (p ^ q))
;
:: thesis: (t | (p ^ q)) . a = ((t | p) | q) . athen
(p ^ q) ^ a in dom t
by A1, A4, TREES_1:def 9;
then A7:
q ^ a in (dom t) | p
by A2, A5, TREES_1:def 9;
then A8:
a in ((dom t) | p) | q
by A3, TREES_1:def 9;
thus (t | (p ^ q)) . a =
t . ((p ^ q) ^ a)
by A4, A6, TREES_2:def 11
.=
(t | p) . (q ^ a)
by A5, A7, TREES_2:def 11
.=
((t | p) | q) . a
by A4, A8, TREES_2:def 11
;
:: thesis: verum end;
hence
t | (p ^ q) = (t | p) | q
by A2, A4, TREES_2:33; :: thesis: verum