theorem Th40: :: MATRIXR2:40

Permutations 0 = {(<*> NAT)}