theorem Th59: :: FINSEQ_2:61

for a being object holds 2 |-> a = <*a,a*>