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

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;

suppose x in dom F ; :: thesis: F . x is FinSequence-like

hence F . x is FinSequence-like by Def3; :: thesis: verum

end;

end;