let F be Field; :: thesis: for E being FieldExtension of F
for L being F -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E)) holds F is Subfield of unionField (S,f,E)
let E be FieldExtension of F; :: thesis: for L being F -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E)) holds F is Subfield of unionField (S,f,E)
let L be F -monomorphic Field; :: thesis: for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E)) holds F is Subfield of unionField (S,f,E)
let f be Monomorphism of F,L; :: thesis: for S being non empty ascending Subset of (Ext_Set (f,E)) holds F is Subfield of unionField (S,f,E)
let S be non empty ascending Subset of (Ext_Set (f,E)); :: thesis: F is Subfield of unionField (S,f,E)
set p = the Element of S;
A2: F is Subfield of the Element of S `1 by FIELD_4:7;
the Element of S `1 is Subfield of unionField (S,f,E) by Fsubb;
hence F is Subfield of unionField (S,f,E) by A2, EC_PF_1:5; :: thesis: verum