theorem Th21: :: NUMBER14:21

for a, b being object
for f being FinSequence holds
( (<*a,b*> ^ f) . 1 = a & (<*a,b*> ^ f) . 2 = b )