theorem Th57: :: FINSEQ_2:59

for a being object holds 1 |-> a = <*a*>