theorem Th73: :: ABCMIZ_0:73

for X being non empty set
for R being Relation of X
for r being RedSequence of R st r . 1 in X holds
r is FinSequence of X