let n be Nat; :: thesis: for R being Relation holds (iter (R,n)) * (id (field R)) = iter (R,n)
let R be Relation; :: thesis: (iter (R,n)) * (id (field R)) = iter (R,n)
rng (iter (R,n)) c= field R by Th71;
hence (iter (R,n)) * (id (field R)) = iter (R,n) by RELAT_1:53; :: thesis: verum