theorem lemID: :: FIELD_16:9

for R being Ring
for S being b₁ -homomorphic Ring
for f being unity-preserving multiplicative Function of R,S
for a being Element of R
for n being Nat holds f . (a |^ n) = (f . a) |^ n