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