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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: (m + n) iter R = (m iter R) (#) (n iter R) ; :: thesis: S₁[n + 1]
thus (m iter R) (#) ((n + 1) iter R) = (m iter R) (#) ((n iter R) (#) R) by Th26
.= ((m + n) iter R) (#) R by A2, LFUZZY_0:23
.= ((m + n) + 1) iter R by Th26
.= (m + (n + 1)) iter R ; :: thesis: verum

end;

(m iter R) (#) (0 iter R) = (m iter R) (#) (Imf (X,X)) by Th24
.= m iter R by Th23 ;
then A3: S₁[ 0 ] ;
for m being Nat holds S₁[m] from NAT_1:sch 2(A3, A1);
hence (m + n) iter R = (m iter R) (#) (n iter R) ; :: thesis: verum