theorem T4a: :: FIELD_11:14

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)