let T be finite-branching DecoratedTree; :: thesis: for x being Element of dom T
for y9 being set st y9 in rng (succ (T,x)) holds
ex x9 being Element of dom T st
( y9 = T . x9 & x9 in succ x )
let x be Element of dom T; :: thesis: for y9 being set st y9 in rng (succ (T,x)) holds
ex x9 being Element of dom T st
( y9 = T . x9 & x9 in succ x )
let y9 be set ; :: thesis: ( y9 in rng (succ (T,x)) implies ex x9 being Element of dom T st
( y9 = T . x9 & x9 in succ x ) )
consider k being Nat such that
A1: dom (succ (T,x)) = Seg k by FINSEQ_1:def 2;
assume y9 in rng (succ (T,x)) ; :: thesis: ex x9 being Element of dom T st
( y9 = T . x9 & x9 in succ x )
then consider n9 being object such that
A2: n9 in dom (succ (T,x)) and
A3: y9 = (succ (T,x)) . n9 by FUNCT_1:def 3;
Seg k = { m where m is Nat : ( 1 <= m & m <= k ) } by FINSEQ_1:def 1;
then consider m9 being Nat such that
A4: n9 = m9 and
A5: 1 <= m9 and
m9 <= k by A2, A1;
m9 <> 0 by A5;
then consider n being Nat such that
A6: n + 1 = m9 by NAT_1:6;
reconsider n = n as Nat ;
n + 1 in dom (x succ) by A2, A4, A6, Th38;
then x ^ <*n*> in dom T by Th39;
then consider x9 being Element of dom T such that
A7: x9 = x ^ <*n*> ;
A8: x9 in succ x by A7;
y9 = T . x9 by A3, A4, A6, A7, Th40;
hence ex x9 being Element of dom T st
( y9 = T . x9 & x9 in succ x ) by A8; :: thesis: verum