reconsider S = N-ZeroStr(# {0},z,f #) as non empty strict N-ZeroStr ;
take S ; :: thesis: ( S is reflexive & S is discerning )
||.(0. S).|| = 0 by FUNCOP_1:7;
hence S is reflexive ; :: thesis: S is discerning
let x be Element of S; :: according to NORMSP_0:def 5 :: thesis: ( ||.x.|| = 0 implies x = 0. S )
thus ( ||.x.|| = 0 implies x = 0. S ) by TARSKI:def 1; :: thesis: verum