let t be finite DecoratedTree; :: thesis: for p being Node of t
for q being Node of (t | p) holds succ t,(p ^ q) = succ (t | p),q
let p be Node of t; :: thesis: for q being Node of (t | p) holds succ t,(p ^ q) = succ (t | p),q
let q be Node of (t | p); :: thesis: succ t,(p ^ q) = succ (t | p),q
A1: dom (t | p) = (dom t) | p by TREES_2:def 11;
then reconsider pq = p ^ q as Element of dom t by TREES_1:def 9;
reconsider q = q as Element of dom (t | p) ;
A2: ( ex q being Element of dom t st
( q = pq & succ t,pq = t * (q succ ) ) & ex r being Element of dom (t | p) st
( r = q & succ (t | p),q = (t | p) * (r succ ) ) ) by Def6;
dom t = (dom t) with-replacement p,((dom t) | p) by TREES_2:8;
then succ pq, succ q are_equipotent by A1, TREES_2:39;
then A3: ( len (pq succ ) = card (succ pq) & len (q succ ) = card (succ q) & card (succ q) = card (succ pq) ) by Def5, CARD_1:21;
then A4: dom (pq succ ) = dom (q succ ) by FINSEQ_3:31;
( rng (pq succ ) c= dom t & rng (q succ ) c= dom (t | p) ) ;
then A5: ( dom (succ t,pq) = dom (pq succ ) & dom (succ (t | p),q) = dom (q succ ) ) by A2, RELAT_1:46;

now

let i be Nat; :: thesis: ( i in dom (q succ ) implies (succ t,pq) . i = (succ (t | p),q) . i )
assume A6: i in dom (q succ ) ; :: thesis: (succ t,pq) . i = (succ (t | p),q) . i
then consider k being Element of NAT such that
A7: ( i = k + 1 & k < len (q succ ) ) by Lm1;
A8: q ^ <*k*> in succ q by A3, A7, Th7;
thus (succ t,pq) . i = t . ((pq succ ) . i) by A2, A4, A5, A6, FUNCT_1:22
.= t . (pq ^ <*k*>) by A3, A7, Def5
.= t . (p ^ (q ^ <*k*>)) by FINSEQ_1:45
.= (t | p) . (q ^ <*k*>) by A1, A8, TREES_2:def 11
.= (t | p) . ((q succ ) . i) by A7, Def5
.= (succ (t | p),q) . i by A2, A5, A6, FUNCT_1:22 ; :: thesis: verum

end;

hence succ t,(p ^ q) = succ (t | p),q by A4, A5, FINSEQ_1:17; :: thesis: verum