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