theorem Th12: :: EUCLID_7:13

for h being FinSequence of REAL holds
( h is one-to-one iff sort_a h is one-to-one )