theorem Th2: :: SIN_COS:2

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