reconsider X = x as set by TARSKI:1;

per cases ( x in dom o or not x in dom o ) ;

suppose x in dom o ; :: thesis: f * (o . x) is FinSequence-like

then o . x in rng o by FUNCT_1:def 3;
then reconsider ox = o . X as FinSequence of dom f by FINSEQ_1:def 11;
A1: rng ox c= dom f ;
dom ox = Seg (len ox) by FINSEQ_1:def 3;
hence f * (o . x) is FinSequence-like by A1, RELAT_1:27; :: thesis: verum

end;

suppose not x in dom o ; :: thesis: f * (o . x) is FinSequence-like

then o . x = {} by FUNCT_1:def 2;
hence f * (o . x) is FinSequence-like ; :: thesis: verum

end;

end;