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_{1}[ Nat] means $1 iter S c= ;

assume A1: S c= ; :: thesis: n iter S c=

A2: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

.= 0 iter S by Th24 ;

then A4: S_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A4, A2);

hence n iter S c= ; :: thesis: verum

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

assume A1: S c= ; :: thesis: n iter S c=

A2: for k being Nat st S

S

proof

0 iter R =
Imf (X,X)
by Th24
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: S_{1}[k]
; :: thesis: S_{1}[k + 1]

( (k iter R) (#) R = (k + 1) iter R & (k iter S) (#) S = (k + 1) iter S ) by Th26;

hence S_{1}[k + 1]
by A1, A3, Th6; :: thesis: verum

end;assume A3: S

( (k iter R) (#) R = (k + 1) iter R & (k iter S) (#) S = (k + 1) iter S ) by Th26;

hence S

.= 0 iter S by Th24 ;

then A4: S

for k being Nat holds S

hence n iter S c= ; :: thesis: verum