let r be Function; :: thesis: ( ( r is finite & r is T-Sequence-like ) iff ex n being Element of NAT st dom r = n )

hereby :: thesis: ( ex n being Element of NAT st dom r = n implies ( r is finite & r is T-Sequence-like ) )

assume ( r is finite & r is T-Sequence-like ) ; :: thesis: ex n being Element of NAT st dom r = n
then ( dom r is finite & dom r is Ordinal ) by FINSET_1:29;
then dom r in omega by CARD_1:103;
hence ex n being Element of NAT st dom r = n ; :: thesis: verum

end;

assume ex n being Element of NAT st dom r = n ; :: thesis: ( r is finite & r is T-Sequence-like )
hence ( r is finite & r is T-Sequence-like ) by FINSET_1:29, ORDINAL1:def 7; :: thesis: verum