set I = Image f;
( the carrier of (Image f) = rng f & the addF of (Image f) = the addF of S || (rng f) & the multF of (Image f) = the multF of S || (rng f) & 1. (Image f) = 1. S & 0. (Image f) = 0. S ) by RING_2:def 6;
hence Image f is strict Subfield of S by EC_PF_1:def 1; :: thesis: verum