set Q = S -sequents ;
set O = OneStep D;
set IT = iter ((OneStep D),m);
iter ((OneStep D),m) is Function of (bool (S -sequents)),(bool (S -sequents)) by FUNCT_7:83;
hence iter ((OneStep D),m) is Rule of S by FUNCT_2:8; :: thesis: verum