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