let R be Relation; :: thesis: for n being Nat holds iter (R,(n + 1)) = R * (iter (R,n))
let n be Nat; :: thesis: iter (R,(n + 1)) = R * (iter (R,n))
consider p being sequence of (bool [:(field R),(field R):]) such that
A1: ( p . (n + 1) = iter (R,(n + 1)) & p . 0 = id (field R) ) and
A2: for k being Nat holds p . (k + 1) = R * (p . k) by Def10;
p . (n + 1) = R * (p . n) by A2;
hence iter (R,(n + 1)) = R * (iter (R,n)) by A1, A2, Def10; :: thesis: verum