theorem eval2: :: FIELD_9:23

for R being non degenerated Ring
for S being RingExtension of R
for a1, b1, c1 being Element of R
for a2, b2, c2 being Element of S st a1 = a2 & b1 = b2 & c1 = c2 holds
<%c2,b2,a2%> = <%c1,b1,a1%>