theorem fresh: :: FIELD_15:40

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