theorem Lm12: :: FIELD_15:44

for p being Prime
for R being commutative b₁ -characteristic Ring
for a, b being Element of R
for x, y being Element of (R |^ p) st a = x & b = y holds
a * b = x * y