per cases ( X <> {} or X = {} ) ;

suppose A1: X <> {} ; :: thesis: f | n is Sequence-like

n c= NAT ;
then n c= dom f by A1, FUNCT_2:def 1;
then dom (f | n) is ordinal by RELAT_1:62;
hence f | n is Sequence-like by ORDINAL1:def 7; :: thesis: verum

end;

suppose X = {} ; :: thesis: f | n is Sequence-like

then f = {} ;
hence f | n is Sequence-like ; :: thesis: verum

end;

end;