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: proj1 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 A2;
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
x in NAT by A3, A2;
then x c= NAT by ORDINAL1:def 2;
then y in NAT by A4;
then reconsider j = y as Nat ;
j < i by A4, NAT_1:44;
hence y in dom F by A1, A3, Def13; :: thesis: verum

end;

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