let F be Function; :: thesis: ( F is initial & F is finite & F is NAT -defined implies F is T-Sequence-like )
assume Z0: ( F is initial & F is finite & F is NAT -defined ) ; :: thesis: F is T-Sequence-like
then XX: 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 Z1: x in dom F ; :: thesis: x c= dom F
then reconsider i = x as Nat by XX;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in x or y in dom F )
assume Z2: y in x ; :: thesis: y in dom F
x in NAT by Z1, XX;
then x c= NAT by ORDINAL1:def 2;
then y in NAT by Z2;
then reconsider j = y as Nat ;
j < i by Z2, NAT_1:45;
hence y in dom F by Z0, Z1, 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 XX;
( x in y or x = y or y in x ) by ORDINAL1:24;
hence ( x in y or x = y or y in x ) ; :: thesis: verum