let m, k be Nat; :: thesis: for R being Relation st iter ((iter (R,m)),k) = iter (R,(m * k)) holds
iter ((iter (R,m)),(k + 1)) = iter (R,(m * (k + 1)))
let R be Relation; :: thesis: ( iter ((iter (R,m)),k) = iter (R,(m * k)) implies iter ((iter (R,m)),(k + 1)) = iter (R,(m * (k + 1))) )
assume A1: iter ((iter (R,m)),k) = iter (R,(m * k)) ; :: thesis: iter ((iter (R,m)),(k + 1)) = iter (R,(m * (k + 1)))
thus iter ((iter (R,m)),(k + 1)) = (iter (R,m)) * (iter ((iter (R,m)),k)) by Th68
.= iter (R,((m * k) + (m * 1))) by A1, Th76
.= iter (R,(m * (k + 1))) ; :: thesis: verum