let s be array; :: thesis: ( s is 0 -based implies s is T-Sequence-like )
assume Z0: for b being ordinal number st b in proj1 s holds
( 0 in proj1 s & 0 c= b ) ; :: according to EXCHSORT:def 2 :: thesis: s is T-Sequence-like
consider c, a being ordinal number such that
A1: dom s = c \ a by SEG;
set x = the Element of c \ a;

now

assume A2: c \ a <> {} ; :: thesis: dom s = c
then the Element of c \ a in c by XBOOLE_0:def 5;
then 0 in dom s by Z0, A1, A2;
then 0 nin a by A1, XBOOLE_0:def 5;
then a c= 0 by ORDINAL6:4;
then a = 0 ;
hence dom s = c by A1; :: thesis: verum

end;

hence dom s is ordinal by A1; :: according to ORDINAL1:def 7 :: thesis: verum