theorem Thm21: :: SRINGS_4:23

for X being non-empty 1 -element FinSequence holds product X = { <*x*> where x is Element of X . 1 : verum }