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) ;
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 A2: card (succ q) = card (succ pq) by CARD_1:21;
A3: ex r being Element of dom (t | p) st
( r = q & succ (t | p),q = (t | p) * (r succ ) ) by Def6;
rng (q succ ) c= dom (t | p) ;
then A4: dom (succ (t | p),q) = dom (q succ ) by A3, RELAT_1:46;
A5: ex q being Element of dom t st
( q = pq & succ t,pq = t * (q succ ) ) by Def6;
rng (pq succ ) c= dom t ;
then A6: dom (succ t,pq) = dom (pq succ ) by A5, RELAT_1:46;
A7: len (q succ ) = card (succ q) by Def5;
A8: len (pq succ ) = card (succ pq) by Def5;
then A9: dom (pq succ ) = dom (q succ ) by A7, A2, FINSEQ_3:31;

now

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

end;

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