let F be Field; :: thesis: for E being FieldExtension of F
for K being FieldExtension of E holds F_Alg K is FieldExtension of F_Alg E
let E be FieldExtension of F; :: thesis: for K being FieldExtension of E holds F_Alg K is FieldExtension of F_Alg E
let K be FieldExtension of E; :: thesis: F_Alg K is FieldExtension of F_Alg E
set FE = F_Alg E;
set FK = F_Alg K;
H0: ( F is Subring of E & E is Subring of K ) by FIELD_4:def 1;
H1: the carrier of (F_Alg E) = Alg_El E by d
.= { a where a is F -algebraic Element of E : verum } ;
H5: the carrier of (F_Alg K) = Alg_El K by d
.= { a where a is E -algebraic Element of K : verum } ;
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 H1;
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;

then H4: [: the carrier of (F_Alg E), the carrier of (F_Alg E):] c= [: the carrier of E, the carrier of E:] by ZFMISC_1:96;

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

let o be object ; :: thesis: ( o in the carrier of (F_Alg E) implies o in the carrier of (F_Alg K) )
assume o in the carrier of (F_Alg E) ; :: thesis: o in the carrier of (F_Alg K)
then consider a being F -algebraic Element of E such that
B: a = o by H1;
@ (a,K) is E -algebraic ;
hence o in the carrier of (F_Alg K) by B, H5; :: thesis: verum

end;

then A: the carrier of (F_Alg E) c= the carrier of (F_Alg K) ;
then H3: [: the carrier of (F_Alg E), the carrier of (F_Alg E):] c= [: the carrier of (F_Alg K), the carrier of (F_Alg K):] by ZFMISC_1:96;
B: the addF of (F_Alg K) || the carrier of (F_Alg E) = ( the addF of K || the carrier of (F_Alg K)) || the carrier of (F_Alg E) by d
.= the addF of K || the carrier of (F_Alg E) by H3, FUNCT_1:51
.= ( the addF of K || the carrier of E) || the carrier of (F_Alg E) by H4, FUNCT_1:51
.= the addF of E || the carrier of (F_Alg E) by H0, C0SP1:def 3
.= the addF of (F_Alg E) by d ;
C: the multF of (F_Alg K) || the carrier of (F_Alg E) = ( the multF of K || the carrier of (F_Alg K)) || the carrier of (F_Alg E) by d
.= the multF of K || the carrier of (F_Alg E) by H3, FUNCT_1:51
.= ( the multF of K || the carrier of E) || the carrier of (F_Alg E) by H4, FUNCT_1:51
.= the multF of E || the carrier of (F_Alg E) by H0, C0SP1:def 3
.= the multF of (F_Alg E) by d ;
D: 1. (F_Alg K) = 1. K by d
.= 1. E by H0, C0SP1:def 3
.= 1. (F_Alg E) by d ;
0. (F_Alg K) = 0. K by d
.= 0. E by H0, C0SP1:def 3
.= 0. (F_Alg E) by d ;
then F_Alg E is Subring of F_Alg K by A, B, C, D, C0SP1:def 3;
hence F_Alg K is FieldExtension of F_Alg E by FIELD_4:def 1; :: thesis: verum