let f be Function; :: thesis: ( f is FinSequence-like implies f is finite )
given n being Nat such that A1: dom f = Seg n ; :: according to FINSEQ_1:def 2 :: thesis: f is finite
rng f is finite by A1, FINSET_1:8;
then [:(dom f),(rng f):] is finite by A1;
hence f is finite by FINSET_1:1, RELAT_1:7; :: thesis: verum