for n being Nat st n >= 1 holds
for m, k, f, ie being Nat st ie is_represented_by n,k & f > 0 holds
for e being Tuple of n, NAT st e = DecSD2 (ie,n,k) holds
(Pow_mod (m,e,f,k)) . n = (m |^ ie) mod f