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 } ;
H2: F is Subring of E by FIELD_4:def 1;
A: the carrier of F c= the carrier of (F_Alg E)

proof

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

let o be object ; :: thesis: ( o in the carrier of F implies o in the carrier of (F_Alg E) )
assume o in the carrier of F ; :: thesis: o in the carrier of (F_Alg E)
then reconsider a = o as Element of F ;
@ (a,E) is F -algebraic ;
hence o in the carrier of (F_Alg E) by H1; :: thesis: verum

end;

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

end;

then Y: [: the carrier of F, the carrier of F:] 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 F = ( the addF of E || the carrier of (F_Alg E)) || the carrier of F by d
.= the addF of E || the carrier of F by Y, FUNCT_1:51
.= the addF of F by H2, C0SP1:def 3 ;
C: the multF of (F_Alg E) || the carrier of F = ( the multF of E || the carrier of (F_Alg E)) || the carrier of F by d
.= the multF of E || the carrier of F by Y, FUNCT_1:51
.= the multF of F by H2, C0SP1:def 3 ;
D: 1. (F_Alg E) = 1. E by d
.= 1. F by H2, C0SP1:def 3 ;
0. (F_Alg E) = 0. E by d
.= 0. F by H2, C0SP1:def 3 ;
then F is Subring of F_Alg E by A, B, C, D, C0SP1:def 3;
hence F_Alg E is F -extending by FIELD_4:def 1; :: thesis: verum