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

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

assume A1: ( r is finite & r is T-Sequence-like ) ; :: thesis: ex n being Nat st dom r = n
then dom r is finite by FINSET_1:10;
hence ex n being Nat st dom r = n by A1; :: thesis: verum

end;

assume ex n being 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:10, ORDINAL1:def 7; :: thesis: verum