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