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 A2: 0 < k ; :: thesis: k !c = ((k -' 1) !c ) * k
A3: 0 + 1 <= k by A2, INT_1:20;
A4: (k -' 1) + 1 = (k - 1) + 1 by A3, XREAL_1:235
.= k ;
thus k !c = ((k -' 1) !c ) * k by A4, Th1; :: thesis: verum

end;

A5: 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)
A7: m <= m + 1 by XREAL_1:31;
A8: (m + 1) -' k = (m + 1) - k by A6, A7, XREAL_1:235, XXREAL_0:2
.= (m - k) + 1
.= (m -' k) + 1 by A6, XREAL_1:235 ;
thus ((m + 1) -' k) !c = ((m -' k) !c ) * (((m -' k) + 1) + (0 * <i> )) by A8, Th1
.= ((m -' k) !c ) * (((m - k) + 1) + (0 * <i> )) by A6, XREAL_1:235
.= ((m -' k) !c ) * ((m + 1) - k) ; :: thesis: verum

end;

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