let R be Field; :: thesis: for E being FieldExtension of R
for x being Element of (F_Alg E) holds x is Element of E
let E be FieldExtension of R; :: thesis: for x being Element of (F_Alg E) holds x is Element of E
let x be Element of (F_Alg E); :: thesis: x is Element of E
A1: the carrier of (F_Alg E) = Alg_El E by d;
x in the carrier of (F_Alg E) ;
hence x is Element of E by A1; :: thesis: verum