set I = Image f;
A:
the carrier of (Image f) = rng f
by defim;
B:
the addF of (Image f) = the addF of S || the carrier of (Image f)
by A, defim;
C:
the multF of (Image f) = the multF of S || the carrier of (Image f)
by A, defim;
D:
1. (Image f) = 1. S
by defim;
0. (Image f) = 0. S
by defim;
hence
Image f is strict Subring of S
by A, B, C, D, C0SP1:def 3; verum