let R be Relation; :: thesis: iter (R,1) = R
thus iter (R,1) = iter (R,(0 + 1))
.= R * (iter (R,0)) by Th68
.= R * (id (field R)) by Th67
.= R by Lm3 ; :: thesis: verum