A1: now

let k be Element of NAT ; :: thesis: ( 0 < k implies k ! = ((k -' 1) ! ) * k )
assume 0 < k ; :: thesis: k ! = ((k -' 1) ! ) * k
then 0 + 1 <= k by INT_1:20;
then (k -' 1) + 1 = (k - 1) + 1 by XREAL_1:235
.= k ;
hence k ! = ((k -' 1) ! ) * k by NEWTON:21; :: thesis: verum

end;

now

let m, k be Element of 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:31;
then (m + 1) -' k = (m + 1) - k by A2, XREAL_1:235, XXREAL_0:2
.= (m - k) + 1
.= (m -' k) + 1 by A2, XREAL_1:235 ;
hence ((m + 1) -' k) ! = ((m -' k) ! ) * ((m -' k) + 1) by NEWTON:21
.= ((m -' k) ! ) * ((m - k) + 1) by A2, XREAL_1:235
.= ((m -' k) ! ) * ((m + 1) - k) ;
:: thesis: verum

end;

hence ( ( for k being Element of NAT st 0 < k holds
((k -' 1) ! ) * k = k ! ) & ( for m, k being Element of NAT st k <= m holds
((m -' k) ! ) * ((m + 1) - k) = ((m + 1) -' k) ! ) ) by A1; :: thesis: verum