let a, e, f be Nat; for n, r, s, t, k being Integer st a |^ e,r are_congruent_mod n & a |^ f,s are_congruent_mod n & r * s = (k * n) + t holds
a |^ (e + f),t are_congruent_mod n
let n, r, s, t, k be Integer; ( a |^ e,r are_congruent_mod n & a |^ f,s are_congruent_mod n & r * s = (k * n) + t implies a |^ (e + f),t are_congruent_mod n )
assume that
A1:
a |^ e,r are_congruent_mod n
and
A2:
a |^ f,s are_congruent_mod n
and
A3:
r * s = (k * n) + t
; a |^ (e + f),t are_congruent_mod n
(a |^ e) * (a |^ f),r * s are_congruent_mod n
by A1, A2, INT_1:18;
then A4:
a |^ (e + f),r * s are_congruent_mod n
by NEWTON:8;
r * s,t are_congruent_mod n
by A3;
hence
a |^ (e + f),t are_congruent_mod n
by A4, INT_1:15; verum