theorem Th68: :: ANPROJ_8:84

for p being FinSequence of 1 -tuples_on REAL st len p = 3 holds
<*<*((p . 1) . 1)*>,<*((p . 2) . 1)*>,<*((p . 3) . 1)*>*> = p