theorem Th20: :: NUMBER14:20

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