let f be Function; :: thesis: ( f is FinSequence-like implies f is segmental )
assume f is FinSequence-like ; :: thesis: f is segmental
then reconsider g = f as FinSequence ;
take a = succ (len g); :: according to EXCHSORT:def 1 :: thesis: ex b being ordinal number st proj1 f = a \ b
take b = 1; :: thesis: proj1 f = a \ b
reconsider c = len g as Nat ;
thus dom f c= a \ b :: according to XBOOLE_0:def 10 :: thesis: a \ b c= proj1 f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in a \ b )
assume A2: x in dom f ; :: thesis: x in a \ b
then x in dom g ;
then reconsider x = x as Nat ;
x <= c by A2, FINSEQ_3:25;
then A1: ( 1 <= x & x <= c ) by A2, FINSEQ_3:25;
then ( succ 0 c= x & x c= c ) by NAT_1:39;
then A3: ( 0 in x & x in a ) by ORDINAL1:21, ORDINAL1:22;
not x in b by A1, CARD_1:49, TARSKI:def 1;
hence x in a \ b by A3, XBOOLE_0:def 5; :: thesis: verum

end;

reconsider d = a as Element of NAT by ORDINAL1:def 12;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in a \ b or x in proj1 f )
assume A5: x in a \ b ; :: thesis: x in proj1 f
then A4: ( x in d & not x in b ) by XBOOLE_0:def 5;
reconsider x = x as Nat by A5;
( x c= c & b c= x ) by A4, ORDINAL1:16, ORDINAL1:22;
then ( 1 <= x & x <= c ) by NAT_1:39;
hence x in proj1 f by FINSEQ_3:25; :: thesis: verum