let s be array; :: thesis: ( s is 0 -based implies s is T-Sequence-like )
assume A1: 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
A2: dom s = c \ a by Def1;
set x = the Element of c \ a;

now :: thesis: ( c \ a <> {} implies dom s = c )

assume A3: 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 A1, A2, A3;
then 0 nin a by A2, XBOOLE_0:def 5;
then a c= 0 by ORDINAL6:4;
then a = 0 ;
hence dom s = c by A2; :: thesis: verum

end;

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