:: deftheorem dRA defines RingAdjunction FIELD_6:def 4 :
for R being Ring
for S being RingExtension of R
for T being Subset of S
for b₄ being strict doubleLoopStr holds
( b₄ = RingAdjunction (R,T) iff ( the carrier of b₄ = carrierRA T & the addF of b₄ = the addF of S || (carrierRA T) & the multF of b₄ = the multF of S || (carrierRA T) & the OneF of b₄ = 1. S & the ZeroF of b₄ = 0. S ) );