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 ) )
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
A1: ( n' in dom (succ T,x) & y' = (succ T,x) . n' ) by FUNCT_1:def 5;
consider k being Nat such that
A2: dom (succ T,x) = Seg k by FINSEQ_1:def 2;
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
A3: ( n' = m' & 1 <= m' & m' <= k ) by A1, A2;
m' <> 0 by A3;
then consider n being Nat such that
A4: 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 A1, A3, A4, Th11;
then x ^ <*n*> in dom T by Th12;
then consider x' being Element of dom T such that
A5: x' = x ^ <*n*> ;
A6: x' in succ x by A5;
y' = T . x' by A1, A3, A4, A5, Th13;
hence ex x' being Element of dom T st
( y' = T . x' & x' in succ x ) by A6; :: thesis: verum