reconsider S = N-ZeroStr(# 1,z,f #) as non empty strict N-ZeroStr ;
take S ; :: thesis: ( S is reflexive & S is discerning )
||.(0. S).|| = 0 by CARD_1:87, FUNCOP_1:13;
hence S is reflexive by Def2; :: 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 CARD_1:87, TARSKI:def 1; :: thesis: verum