theorem :: FIELD_4:14

for R being Ring
for S being RingExtension of R holds 1_. S = 1_. R