theorem T4: :: FIELD_11:15

for n being Ordinal
for R being non degenerated Ring
for a, b being Element of R holds (a | (n,R)) *' (b | (n,R)) = (a * b) | (n,R)