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

proof

assume f is non-zero ; :: thesis: rng f c= NonZero S
then not 0. S in rng f by STRUCT_0:def 15;
hence rng f c= NonZero S by ZFMISC_1:34; :: thesis: verum

end;

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