let f be Function; :: thesis: ( f is Sequence-like implies f is segmental )
assume f is Sequence-like ; :: thesis: f is segmental
then reconsider f = f as Sequence ;
take dom f ; :: according to EXCHSORT:def 1 :: thesis: ex b being Ordinal st proj1 f = (dom f) \ b
take 0 ; :: thesis: proj1 f = (dom f) \ 0
thus proj1 f = (dom f) \ 0 ; :: thesis: verum