let R be Relation; :: thesis: ( R is empty implies R is FinSequence-like )
assume A1: R is empty ; :: thesis: R is FinSequence-like
take 0 ; :: according to FINSEQ_1:def 2 :: thesis: dom R = Seg 0
thus dom R = Seg 0 by A1; :: thesis: verum