theorem Th4: :: RING_EMB:4

for A being Ring
for X being non empty set
for f being Function of A,X
for a, b, c being Element of X st f is bijective holds
addemb (f,a,(addemb (f,b,c))) = addemb (f,(addemb (f,a,b)),c)