:: deftheorem defines non-vanishing FUZIMPL3:def 14 :
for N being UnOp of [.0,1.] holds
( N is non-vanishing iff for x being Element of [.0,1.] holds
( N . x = 0 iff x = 1 ) );