let k, m be Element of NAT ; :: thesis: ( ( 0 < k implies ((k -' 1) !c ) * k = k !c ) & ( k <= m implies ((m -' k) !c ) * ((m + 1) - k) = ((m + 1) -' k) !c ) )

A1: now

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

end;

now

let m, k be Element of NAT ; :: thesis: ( k <= m implies ((m + 1) -' k) !c = ((m -' k) !c ) * ((m + 1) - k) )
assume A6: k <= m ; :: thesis: ((m + 1) -' k) !c = ((m -' k) !c ) * ((m + 1) - k)
m <= m + 1 by XREAL_1:31;
then (m + 1) -' k = (m + 1) - k by A6, XREAL_1:235, XXREAL_0:2
.= (m - k) + 1
.= (m -' k) + 1 by A6, XREAL_1:235 ;
hence ((m + 1) -' k) !c = ((m -' k) !c ) * (((m -' k) + 1) + (0 * <i> )) by Th1
.= ((m -' k) !c ) * (((m - k) + 1) + (0 * <i> )) by A6, XREAL_1:235
.= ((m -' k) !c ) * ((m + 1) - k) ;
:: thesis: verum

end;

hence ( ( 0 < k implies ((k -' 1) !c ) * k = k !c ) & ( k <= m implies ((m -' k) !c ) * ((m + 1) - k) = ((m + 1) -' k) !c ) ) by A1; :: thesis: verum