let F be Function; :: thesis: ( F is initial & F is finite & F is NAT -defined implies F is Sequence-like )
assume A1: ( F is initial & F is finite & F is NAT -defined ) ; :: thesis: F is Sequence-like
thus dom F is epsilon-transitive :: according to ORDINAL1:def 4,ORDINAL1:def 7 :: thesis: dom F is epsilon-connected

proof

let x be set ; :: according to ORDINAL1:def 2 :: thesis: ( not x in dom F or x c= dom F )
assume A2: x in dom F ; :: thesis: x c= dom F
then reconsider i = x as Nat by A1;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in x or y in dom F )
assume y in x ; :: thesis: y in dom F
then A3: y in Segm i ;
then reconsider j = y as Nat ;
thus y in dom F by A1, A2, NAT_1:44, A3; :: thesis: verum

end;

let x, y be set ; :: according to ORDINAL1:def 3 :: thesis: ( not x in dom F or not y in dom F or x in y or x = y or y in x )
assume ( x in dom F & y in dom F ) ; :: thesis: ( x in y or x = y or y in x )
then reconsider x = x, y = y as Ordinal by A1;
( x in y or x = y or y in x ) by ORDINAL1:14;
hence ( x in y or x = y or y in x ) ; :: thesis: verum