let F be Field; :: thesis: for E being F -algebraic FieldExtension of F holds F_Alg E is FieldExtension of E
let E be F -algebraic FieldExtension of F; :: thesis: F_Alg E is FieldExtension of E
set FE = F_Alg E;
H1: the carrier of (F_Alg E) = Alg_El E by d
.= { a where a is F -algebraic Element of E : verum } ;
A: the carrier of E c= the carrier of (F_Alg E) by H1;
then H3: [: the carrier of E, the carrier of E:] c= [: the carrier of (F_Alg E), the carrier of (F_Alg E):] by ZFMISC_1:96;
B: the addF of (F_Alg E) || the carrier of E = ( the addF of E || the carrier of (F_Alg E)) || the carrier of E by d
.= the addF of E || the carrier of E by H3, FUNCT_1:51 ;
C: the multF of (F_Alg E) || the carrier of E = ( the multF of E || the carrier of (F_Alg E)) || the carrier of E by d
.= the multF of E || the carrier of E by H3, FUNCT_1:51 ;
D: 1. (F_Alg E) = 1. E by d;
0. (F_Alg E) = 0. E by d;
then E is Subring of F_Alg E by A, B, C, D, C0SP1:def 3;
hence F_Alg E is FieldExtension of E by FIELD_4:def 1; :: thesis: verum