theorem pr20: :: FIELD_6:20

for S being Ring
for R being Subring of S
for x1, x2 being Element of S
for y1, y2 being Element of R st x1 = y1 & x2 = y2 holds
<%x1,x2%> = <%y1,y2%>