let t be finite-branching DecoratedTree; 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; for q being Node of (t | p) holds succ (t,(p ^ q)) = succ ((t | p),q)
let q be Node of (t | p); succ (t,(p ^ q)) = succ ((t | p),q)
A1:
dom (t | p) = (dom t) | p
by TREES_2:def 10;
then reconsider pq = p ^ q as Element of dom t by TREES_1:def 6;
reconsider q = q as Element of dom (t | p) ;
dom t = (dom t) with-replacement (p,((dom t) | p))
by TREES_2:6;
then
succ pq, succ q are_equipotent
by A1, TREES_2:37;
then A2:
card (succ q) = card (succ pq)
by CARD_1:5;
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:27;
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:27;
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:29;
now for i being Nat st i in dom (q succ) holds
(succ (t,pq)) . i = (succ ((t | p),q)) . ilet i be
Nat;
( i in dom (q succ) implies (succ (t,pq)) . i = (succ ((t | p),q)) . i )assume A10:
i in dom (q succ)
;
(succ (t,pq)) . i = (succ ((t | p),q)) . ithen consider k being
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;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
thus (succ (t,pq)) . i =
t . ((pq succ) . i)
by A5, A9, A6, A10, FUNCT_1:12
.=
t . (pq ^ <*k*>)
by A8, A7, A2, A11, A12, Def5
.=
t . (p ^ (q ^ <*k*>))
by FINSEQ_1:32
.=
(t | p) . (q ^ <*k*>)
by A1, A13, TREES_2:def 10
.=
(t | p) . ((q succ) . i)
by A11, A12, Def5
.=
(succ ((t | p),q)) . i
by A3, A4, A10, FUNCT_1:12
;
verum end;
hence
succ (t,(p ^ q)) = succ ((t | p),q)
by A9, A6, A4; verum