let s, t be DecoratedTree; for x being object
for q being FinSequence of NAT st q in dom s holds
(x -tree (t,s)) . (<*1*> ^ q) = s . q
let x be object ; for q being FinSequence of NAT st q in dom s holds
(x -tree (t,s)) . (<*1*> ^ q) = s . q
let q be FinSequence of NAT ; ( q in dom s implies (x -tree (t,s)) . (<*1*> ^ q) = s . q )
assume A1:
q in dom s
; (x -tree (t,s)) . (<*1*> ^ q) = s . q
set r = <*t,s*>;
A2:
len <*t,s*> = 2
by FINSEQ_1:44;
A3: (x -tree (t,s)) | <*1*> =
<*t,s*> . (1 + 1)
by A2, TREES_4:def 4
.=
s
by FINSEQ_1:44
;
dom ((x -tree (t,s)) | <*1*>) = (dom (x -tree (t,s))) | <*1*>
by TREES_2:def 10;
hence
(x -tree (t,s)) . (<*1*> ^ q) = s . q
by A1, A3, TREES_2:def 10; verum