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
then dom R is ordinal by ORDINAL1:def 7;
hence R is with_cardinal_domain by A1; :: thesis: verum