theorem EZ: :: NEWTON04:72

for k, n being Nat holds
( (n !) * (k !) = (n + k) ! iff ( n = 0 or k = 0 ) )