consider f being FinSequence, I being set ;
A1: dom (I --> f) = I by FUNCOP_1:19;
take F = I --> f; :: thesis: F is FinSequence-yielding
let x be set ; :: according to MATRLIN:def 1 :: thesis: ( x in dom F implies F . x is FinSequence )
assume x in dom F ; :: thesis: F . x is FinSequence
hence F . x is FinSequence by A1, FUNCOP_1:13; :: thesis: verum