let f be Sequence; :: thesis: ( f is infinite iff omega c= dom f )
( f is infinite iff dom f is infinite ) by FINSET_1:10;
hence ( f is infinite iff omega c= dom f ) by CARD_3:85; :: thesis: verum