let K be Field; :: thesis: K is Subfield of K
A1: the addF of K = the addF of K || the carrier of K ;
A2: the multF of K = the multF of K || the carrier of K ;
( the carrier of K c= the carrier of K & 1. K = 1. K & 0. K = 0. K ) ;
hence K is Subfield of K by A1, A2, EC_PF_1:def 1; :: thesis: verum