theorem :: FIELD_15:41

for p being Prime
for R being commutative b₁ -characteristic Ring
for a, b being Element of R
for i being Nat holds (a + b) |^ (p |^ i) = (a |^ (p |^ i)) + (b |^ (p |^ i))