let R be Relation; :: thesis: ( R is finite & R is Sequence-like implies R is with_cardinal_domain )
assume A1: ( R is finite & R is Sequence-like ) ; :: thesis: R is with_cardinal_domain
( dom R is epsilon-transitive & dom R is epsilon-connected ) by A1, ORDINAL1:def 7;
hence R is with_cardinal_domain by A1; :: thesis: verum