theorem Th8: :: FIELD_4:12

for R, S being Ring st S is RingExtension of R holds
0_. S = 0_. R