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:29;
hence ( not f is finite iff omega c= dom f ) by CARD_3:102; :: thesis: verum