let t be finite-branching Tree; :: thesis:
let p be Element of t; :: thesis:
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)

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

end;

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

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

end;

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

let i, j be Nat; :: thesis:
assume p ^ <*i*> = p ^ <*j*> ; :: thesis:
hence i = (p ^ <*j*>) . ((len p) + 1) by FINSEQ_1:42
.= j by FINSEQ_1:42 ;
:: thesis:

end;