let s be array; :: thesis: ( s is 0 -based implies s is Sequence-like )
assume A1: for b being Ordinal st b in proj1 s holds
( 0 in proj1 s & 0 c= b ) ; :: according to EXCHSORT:def 2 :: thesis: s is Sequence-like
consider c, a being Ordinal 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 epsilon-transitive & dom s is epsilon-connected ) by A2; :: according to ORDINAL1:def 7 :: thesis: verum