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 p being Element of Ext_Set (f,E) holds p <= p
let E be FieldExtension of F; :: thesis: for L being F -monomorphic Field
for f being Monomorphism of F,L
for p being Element of Ext_Set (f,E) holds p <= p
let L be F -monomorphic Field; :: thesis: for f being Monomorphism of F,L
for p being Element of Ext_Set (f,E) holds p <= p
let f be Monomorphism of F,L; :: thesis: for p being Element of Ext_Set (f,E) holds p <= p
let p be Element of Ext_Set (f,E); :: thesis: p <= p
for K being FieldExtension of p `1
for g being Function of K,L st K = p `1 & g = p `2 holds
g is p `2 -extending ;
hence p <= p by FIELD_4:6; :: thesis: verum