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 )
A2: k in NAT by ORDINAL1:def 12;
assume 0 < k ; :: thesis: k ! = ((k -' 1) !) * k
then 0 + 1 <= k by INT_1:7, A2;
then (k -' 1) + 1 = (k - 1) + 1 by XREAL_1:233
.= k ;
hence k ! = ((k -' 1) !) * k by NEWTON:15; :: 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 A3: 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 A3, XREAL_1:233, XXREAL_0:2
.= (m - k) + 1
.= (m -' k) + 1 by A3, XREAL_1:233 ;
hence ((m + 1) -' k) ! = ((m -' k) !) * ((m -' k) + 1) by NEWTON:15
.= ((m -' k) !) * ((m - k) + 1) by A3, XREAL_1:233
.= ((m -' k) !) * ((m + 1) - k) ;
:: thesis: verum

end;

hence ( ( 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) ! ) ) by A1; :: thesis: verum