let t be finite-branching Tree; :: thesis: for p being Element of t
for n being Element of NAT holds
( p ^ <*n*> in succ p iff n < card (succ p) )
let p be Element of t; :: thesis: for n being Element of NAT holds
( p ^ <*n*> in succ p iff n < card (succ p) )
deffunc H₁( Element of NAT ) -> FinSequence of NAT = p ^ <*$1*>;
A1: for x being set st x in succ p holds
ex n being Element of NAT st x = H₁(n)

proof

let x be set ; :: thesis: ( x in succ p implies ex n being Element of NAT st x = H₁(n) )
assume x in succ p ; :: thesis: ex n being Element of NAT st x = H₁(n)
then ex n being Element of NAT st
( x = H₁(n) & H₁(n) in t ) ;
hence ex n being Element of NAT st x = H₁(n) ; :: thesis: verum

end;

A2: for i, j being Element of NAT st i < j & H₁(j) in succ p holds
H₁(i) in succ p

proof

let i, j be Element of NAT ; :: thesis: ( i < j & H₁(j) in succ p implies H₁(i) in succ p )
assume ( i < j & p ^ <*j*> in succ p ) ; :: thesis: H₁(i) in succ p
then p ^ <*i*> in t by TREES_1:def 5;
hence H₁(i) in succ p ; :: thesis: verum

end;

A3: for i, j being Element of NAT st H₁(i) = H₁(j) holds
i = j

proof

let i, j be Element of NAT ; :: thesis: ( H₁(i) = H₁(j) implies i = j )
assume p ^ <*i*> = p ^ <*j*> ; :: thesis: i = j
hence i = (p ^ <*j*>) . ((len p) + 1) by FINSEQ_1:59
.= j by FINSEQ_1:59 ;
:: thesis: verum

end;

thus for n being Element of NAT holds
( H₁(n) in succ p iff n < card (succ p) ) from TREES_9:sch 1(A1, A2, A3); :: thesis: verum