let X be non empty set ; :: thesis: for R, S being RMembership_Func of X,X
for n being Nat st S c= holds
n iter S c=
let R, S be RMembership_Func of X,X; :: thesis: for n being Nat st S c= holds
n iter S c=
let n be Nat; :: thesis: ( S c= implies n iter S c= )
defpred S₁[ Nat] means $1 iter S c= ;
assume A1: S c= ; :: thesis: n iter S c=
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
( (k iter R) (#) R = (k + 1) iter R & (k iter S) (#) S = (k + 1) iter S ) by Th26;
hence S₁[k + 1] by A1, A3, Th6; :: thesis: verum

end;

0 iter R = Imf (X,X) by Th24
.= 0 iter S by Th24 ;
then A4: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A2);
hence n iter S c= ; :: thesis: verum