theorem lem4: :: FIELD_12:15

for f being Field-yielding ascending sequence
for a, b being Element of (SeqField f)
for i being Element of NAT
for x, y being Element of (f . i) st x = a & y = b holds
( a + b = x + y & a * b = x * y )