thus
( f is non-zero implies rng f c= NonZero S )
by ZFMISC_1:34; :: thesis: ( rng f c= NonZero S implies f is non-zero )

assume A1: rng f c= NonZero S ; :: thesis: f is non-zero

assume 0. S in rng f ; :: according to STRUCT_0:def 15 :: thesis: contradiction

then not 0. S in {(0. S)} by A1, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

assume A1: rng f c= NonZero S ; :: thesis: f is non-zero

assume 0. S in rng f ; :: according to STRUCT_0:def 15 :: thesis: contradiction

then not 0. S in {(0. S)} by A1, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum