let m, n be Nat; :: thesis: for t being Integer holds t |^ n,t |^ m are_congruent_mod t - 1
let t be Integer; :: thesis: t |^ n,t |^ m are_congruent_mod t - 1

per cases ( n >= m or m >= n ) ;

suppose n >= m ; :: thesis: t |^ n,t |^ m are_congruent_mod t - 1

then consider k being Nat such that
B2: n = m + k by NAT_1:10;
t |^ (m + k) = (t |^ m) * (t |^ k) by NEWTON:8;
then (t |^ (m + k)) - (t |^ m) = (t |^ m) * ((t |^ k) - (1 |^ k)) ;
hence t |^ n,t |^ m are_congruent_mod t - 1 by B2, Th18, INT_2:2; :: thesis: verum

end;

suppose m >= n ; :: thesis: t |^ n,t |^ m are_congruent_mod t - 1

then consider k being Nat such that
B2: m = n + k by NAT_1:10;
t |^ (n + k) = (t |^ n) * (t |^ k) by NEWTON:8;
then (t |^ (n + k)) - (t |^ n) = (t |^ n) * ((t |^ k) - (1 |^ k)) ;
then t - 1 divides (t |^ m) - (t |^ n) by B2, Th18, INT_2:2;
then t - 1 divides - ((- (t |^ n)) + (t |^ m)) by INT_2:10;
hence t |^ n,t |^ m are_congruent_mod t - 1 ; :: thesis: verum

end;

end;