let F be Field; :: thesis: for E being FieldExtension of F holds E,E are_isomorphic_over F
let E be FieldExtension of F; :: thesis: E,E are_isomorphic_over F
now :: thesis: for a being Element of F holds (id E) . a = a
let a be Element of F; :: thesis: (id E) . a = a
F is Subring of E by FIELD_4:def 1;
then the carrier of F c= the carrier of E by C0SP1:def 3;
hence (id E) . a = a by FUNCT_1:18; :: thesis: verum
end;
then id E is F -fixing ;
then id E is F -isomorphism ;
hence E,E are_isomorphic_over F ; :: thesis: verum