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

proof

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

end;

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

proof

let i, j be Nat; :: thesis: ( i < j & H₁(j) in succ p implies H₁(i) in succ p )
assume A3: ( i < j & p ^ <*j*> in succ p ) ; :: thesis: H₁(i) in succ p
reconsider i = i, j = j as Nat ;
p ^ <*i*> in t by A3, TREES_1:def 3;
hence H₁(i) in succ p ; :: thesis: verum

end;

A4: for i, j being Nat st H₁(i) = H₁(j) holds
i = j

proof

let i, j be 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:42
.= j by FINSEQ_1:42 ;
:: thesis: verum

end;

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