let E be Field; :: thesis: for F being Subfield of E holds F is Subring of E

let F be Subfield of E; :: thesis: F is Subring of E

( the carrier of F c= the carrier of E & the addF of F = the addF of E || the carrier of F & the multF of F = the multF of E || the carrier of F & 1. E = 1. F & 0. E = 0. F ) by EC_PF_1:def 1;

hence F is Subring of E by C0SP1:def 3; :: thesis: verum

let F be Subfield of E; :: thesis: F is Subring of E

( the carrier of F c= the carrier of E & the addF of F = the addF of E || the carrier of F & the multF of F = the multF of E || the carrier of F & 1. E = 1. F & 0. E = 0. F ) by EC_PF_1:def 1;

hence F is Subring of E by C0SP1:def 3; :: thesis: verum