let R be Ring; :: thesis: for S being RingExtension of R
for T being Subset of S
for a, b being Element of S
for x, y being Element of (RAdj (R,T)) st a = x & b = y holds
a + b = x + y
let S be RingExtension of R; :: thesis: for T being Subset of S
for a, b being Element of S
for x, y being Element of (RAdj (R,T)) st a = x & b = y holds
a + b = x + y
let T be Subset of S; :: thesis: for a, b being Element of S
for x, y being Element of (RAdj (R,T)) st a = x & b = y holds
a + b = x + y
let a, b be Element of S; :: thesis: for x, y being Element of (RAdj (R,T)) st a = x & b = y holds
a + b = x + y
let x, y be Element of (RAdj (R,T)); :: thesis: ( a = x & b = y implies a + b = x + y )
assume A1: ( a = x & b = y ) ; :: thesis: a + b = x + y
the carrier of (RAdj (R,T)) = carrierRA T by dRA;
hence a + b = ( the addF of S || (carrierRA T)) . (x,y) by A1, RING_3:1
.= x + y by dRA ;
:: thesis: verum