let F be Field; :: thesis: for E being FieldExtension of F holds E is FieldExtension of F_Alg E
let E be FieldExtension of F; :: thesis: E is FieldExtension of F_Alg E
set FE = F_Alg E;
H: 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 (F_Alg E) c= the carrier of E

proof

now :: thesis: for o being object st o in the carrier of (F_Alg E) holds
o in the carrier of E

let o be object ; :: thesis: ( o in the carrier of (F_Alg E) implies o in the carrier of E )
assume o in the carrier of (F_Alg E) ; :: thesis: o in the carrier of E
then consider a being F -algebraic Element of E such that
B: a = o by H;
thus o in the carrier of E by B; :: thesis: verum

end;

hence the carrier of (F_Alg E) c= the carrier of E ; :: thesis: verum

end;

( the addF of (F_Alg E) = the addF of E || the carrier of (F_Alg E) & the multF of (F_Alg E) = the multF of E || the carrier of (F_Alg E) & 1. (F_Alg E) = 1. E & 0. (F_Alg E) = 0. E ) by d;
then F_Alg E is Subring of E by A, C0SP1:def 3;
hence E is FieldExtension of F_Alg E by FIELD_4:def 1; :: thesis: verum