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

end;

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;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