per cases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; :: thesis: f . x is FinSequence-like
then A1: f . x in rng f by FUNCT_1:def 3;
rng f c= D by RELAT_1:def 19;
hence f . x is FinSequence-like by A1; :: thesis: verum
end;
suppose not x in dom f ; :: thesis: f . x is FinSequence-like
hence f . x is FinSequence-like by FUNCT_1:def 2; :: thesis: verum
end;
end;