let T be finite-branching DecoratedTree; :: thesis: for x being Element of dom T
for y' being set st y' in rng (succ T,x) holds
ex x' being Element of dom T st
( y' = T . x' & x' in succ x )
let x be Element of dom T; :: thesis: for y' being set st y' in rng (succ T,x) holds
ex x' being Element of dom T st
( y' = T . x' & x' in succ x )
let y' be set ; :: thesis: ( y' in rng (succ T,x) implies ex x' being Element of dom T st
( y' = T . x' & x' in succ x ) )
consider k being Nat such that
A1: dom (succ T,x) = Seg k by FINSEQ_1:def 2;
assume y' in rng (succ T,x) ; :: thesis: ex x' being Element of dom T st
( y' = T . x' & x' in succ x )
then consider n' being set such that
A2: n' in dom (succ T,x) and
A3: y' = (succ T,x) . n' by FUNCT_1:def 5;
Seg k = { m where m is Element of NAT : ( 1 <= m & m <= k ) } by FINSEQ_1:def 1;
then consider m' being Element of NAT such that
A4: n' = m' and
A5: 1 <= m' and
m' <= k by A2, A1;
m' <> 0 by A5;
then consider n being Nat such that
A6: n + 1 = m' by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
n + 1 in dom (x succ ) by A2, A4, A6, Th11;
then x ^ <*n*> in dom T by Th12;
then consider x' being Element of dom T such that
A7: x' = x ^ <*n*> ;
A8: x' in succ x by A7;
y' = T . x' by A3, A4, A6, A7, Th13;
hence ex x' being Element of dom T st
( y' = T . x' & x' in succ x ) by A8; :: thesis: verum