theorem Th13: :: LOPBAN_4:13

( ( for k being Nat st 0 < k holds
((k -' 1) !) * k = k ! ) & ( for m, k being Nat st k <= m holds
((m -' k) !) * ((m + 1) - k) = ((m + 1) -' k) ! ) )