let L be non empty 1-sorted ; :: thesis: for f being bijective Function of L,L
for n, m being Nat holds
( f `^ (n + 1) = f `^ (m + 1) iff f `^ n = f `^ m )
let f be bijective Function of L,L; :: thesis: for n, m being Nat holds
( f `^ (n + 1) = f `^ (m + 1) iff f `^ n = f `^ m )
let n, m be Nat; :: thesis: ( f `^ (n + 1) = f `^ (m + 1) iff f `^ n = f `^ m )
H: f is onto ;

A: now :: thesis: ( f `^ (n + 1) = f `^ (m + 1) implies f `^ m = f `^ n )

assume f `^ (n + 1) = f `^ (m + 1) ; :: thesis: f `^ m = f `^ n
then ((f `^ n) * f) * (f ") = (f `^ (m + 1)) * (f ") by T3
.= ((f `^ m) * f) * (f ") by T3
.= (f `^ m) * (f * (f ")) by T2
.= (f `^ m) * (id L) by H, FUNCT_1:39
.= f `^ m ;
hence f `^ m = (f `^ n) * (f * (f ")) by T2
.= (f `^ n) * (id L) by H, FUNCT_1:39
.= f `^ n ;
:: thesis: verum

end;

now :: thesis: ( f `^ n = f `^ m implies f `^ (n + 1) = f `^ (m + 1) )

assume f `^ n = f `^ m ; :: thesis: f `^ (n + 1) = f `^ (m + 1)
hence f `^ (n + 1) = (f `^ m) * f by T3
.= f `^ (m + 1) by T3 ;
:: thesis: verum

end;

hence ( f `^ (n + 1) = f `^ (m + 1) iff f `^ n = f `^ m ) by A; :: thesis: verum