for X being finite set holds
( proj1 X is finite & proj2 X is finite )