let k, m be Nat; :: thesis: ( ( 0 < k implies ((k -' 1) !) * k = k ! ) & ( k <= m implies ((m -' k) !) * ((m + 1) - k) = ((m + 1) -' k) ! ) )
A1: now :: thesis: for k being Nat st 0 < k holds
k ! = ((k -' 1) !) * k
let k be Nat; :: thesis: ( 0 < k implies k ! = ((k -' 1) !) * k )
assume 0 < k ; :: thesis: k ! = ((k -' 1) !) * k
then 0 + 1 <= k by INT_1:7;
then (k -' 1) + 1 = (k - 1) + 1 by XREAL_1:233
.= k ;
hence k ! = ((k -' 1) !) * k by Th1; :: thesis: verum
end;
now :: thesis: for m, k being Nat st k <= m holds
((m + 1) -' k) ! = ((m -' k) !) * ((m + 1) - k)
let m, k be Nat; :: thesis: ( k <= m implies ((m + 1) -' k) ! = ((m -' k) !) * ((m + 1) - k) )
assume A2: k <= m ; :: thesis: ((m + 1) -' k) ! = ((m -' k) !) * ((m + 1) - k)
m <= m + 1 by XREAL_1:29;
then (m + 1) -' k = (m + 1) - k by A2, XREAL_1:233, XXREAL_0:2
.= (m - k) + 1
.= (m -' k) + 1 by A2, XREAL_1:233 ;
hence ((m + 1) -' k) ! = ((m -' k) !) * (((m -' k) + 1) + (0 * <i>)) by Th1
.= ((m -' k) !) * (((m - k) + 1) + (0 * <i>)) by A2, XREAL_1:233
.= ((m -' k) !) * ((m + 1) - k) ;
:: thesis: verum
end;
hence ( ( 0 < k implies ((k -' 1) !) * k = k ! ) & ( k <= m implies ((m -' k) !) * ((m + 1) - k) = ((m + 1) -' k) ! ) ) by A1; :: thesis: verum