let f be Function; :: thesis: for m, k being Element of NAT st iter (iter f,m),k = iter f,(m * k) holds
iter (iter f,m),(k + 1) = iter f,(m * (k + 1))
let m, k be Element of NAT ; :: thesis: ( iter (iter f,m),k = iter f,(m * k) implies iter (iter f,m),(k + 1) = iter f,(m * (k + 1)) )
assume A1: iter (iter f,m),k = iter f,(m * k) ; :: thesis: iter (iter f,m),(k + 1) = iter f,(m * (k + 1))
thus iter (iter f,m),(k + 1) = (iter (iter f,m),k) * (iter f,m) by Th71
.= iter f,((m * k) + (m * 1)) by A1, Th79
.= iter f,(m * (k + 1)) ; :: thesis: verum