theorem lem5a: :: FIELD_12:51

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 p being Element of S holds
( 1. (unionField (S,f,E)) = 1. (p `1) & 0. (unionField (S,f,E)) = 0. (p `1) )