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