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 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in a \ b )
assume A1: x in dom f ; :: thesis: x in a \ b
then x in dom g ;
then reconsider x = x as Nat ;
x <= c by A1, FINSEQ_3:25;
then A2: ( 1 <= x & x <= c ) by A1, FINSEQ_3:25;
then ( Segm (succ 0) c= Segm x & Segm x c= Segm c ) by NAT_1:39;
then A3: ( 0 in x & x in a ) by ORDINAL1:22;
not x in b by A2, 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in a \ b or x in proj1 f )
assume x in a \ b ; :: thesis: x in proj1 f
then A4: ( x in d & not x in b ) by XBOOLE_0:def 5;
then x in Segm d ;
then reconsider x = x as Nat ;
( Segm x c= Segm c & Segm b c= Segm 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