theorem :: AFINSQ_1:5

for r being Function holds
( ( r is finite & r is Sequence-like ) iff ex n being Nat st dom r = n ) by FINSET_1:10;