let F be Function; :: thesis: ( F is initial & F is finite & F is NAT -defined implies F is T-Sequence-like )
assume A1: ( F is initial & F is finite & F is NAT -defined ) ; :: thesis: F is T-Sequence-like
then A2: dom F c= NAT by RELAT_1:def 18;
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 A3: x in dom F ; :: thesis: x c= dom F
then reconsider i = x as Nat by A1;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in x or y in dom F )
assume A4: y in x ; :: thesis: y in dom F
reconsider j = y as Nat by A4, A3, A2;
j < i by A4, NAT_1:44;
hence y in dom F by A1, A3, Def12; :: thesis: verum

end;

let x be set ; :: according to ORDINAL1:def 3 :: thesis: for b₁ being set holds
( not x in dom F or not b₁ in dom F or x in b₁ or x = b₁ or b₁ in x )
let y be set ; :: 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