let R be Relation; :: thesis: iter (R,0) = id (field R)
ex p being sequence of (bool [:(field R),(field R):]) st
( iter (R,0) = p . 0 & p . 0 = id (field R) & ( for k being Nat holds p . (k + 1) = R * (p . k) ) ) by Def10;
hence iter (R,0) = id (field R) ; :: thesis: verum