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