theorem t4a: :: FIELD_15:23

for R being domRing
for a being non zero Element of R
for n being Nat holds <%(0. R),a%> `^ n = (a |^ n) * (<%(0. R),(1. R)%> `^ n)