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