let L be non empty 1-sorted ; :: thesis: for f being bijective Function of L,L
for n, m, k being Nat st f `^ n = f `^ m & k = n - m holds
f `^ k = f `^ 0
let f be bijective Function of L,L; :: thesis: for n, m, k being Nat st f `^ n = f `^ m & k = n - m holds
f `^ k = f `^ 0
let n, m, k be Nat; :: thesis: ( f `^ n = f `^ m & k = n - m implies f `^ k = f `^ 0 )
assume AS: ( f `^ n = f `^ m & k = n - m ) ; :: thesis: f `^ k = f `^ 0
defpred S₁[ Nat] means for n, k being Nat st f `^ n = f `^ $1 & k = n - $1 holds
f `^ k = f `^ 0;
IA: S₁[ 0 ] ;

IS: now :: thesis: for m being Nat st S₁[m] holds
S₁[m + 1]

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume IV: S₁[m] ; :: thesis: S₁[m + 1]

now :: thesis: for n, k being Nat st f `^ n = f `^ (m + 1) & k = n - (m + 1) holds
f `^ 0 = f `^ k

let n, k be Nat; :: thesis: ( f `^ n = f `^ (m + 1) & k = n - (m + 1) implies f `^ 0 = f `^ k )
assume AS: ( f `^ n = f `^ (m + 1) & k = n - (m + 1) ) ; :: thesis: f `^ 0 = f `^ k
then (n - (m + 1)) + m >= 0 + m by XREAL_1:6;
then reconsider n1 = n - 1 as Element of NAT by INT_1:3;
reconsider k1 = n1 - m as Nat by AS;
n = n1 + 1 ;
then f `^ n1 = f `^ m by AS, TT2;
hence f `^ 0 = f `^ k1 by IV
.= f `^ k by AS ;
:: thesis: verum

end;

hence S₁[m + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
hence f `^ k = f `^ 0 by AS; :: thesis: verum