theorem lemiso: :: VECTSP13:1

for X, Y being non empty finite set st card Y = card X holds
ex f being Function of X,Y st f is bijective