theorem lem4a: :: FIELD_12:52

for F being Field
for E being FieldExtension of F
for L being b₁ -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E))
for a, b being Element of (unionField (S,f,E))
for p being Element of S
for x, y being Element of (p `1) st x = a & y = b holds
( a + b = x + y & a * b = x * y )