let s, t be DecoratedTree; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( q in dom t implies (x -tree (t,s)) . (<*0*> ^ q) = t . q )
assume A1: q in dom t ; :: thesis: (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 ;
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; :: thesis: verum