theorem lem2: :: FIELD_12:13

for f being Field-yielding ascending sequence
for i, j being Element of NAT
for xi, yi being Element of (f . i)
for xj, yj being Element of (f . j) st xi = xj & yi = yj holds
( xi + yi = xj + yj & xi * yi = xj * yj )