consider A being non empty set , Z being Element of A, a being BinOp of A, M being Function of [:REAL ,A:],A, n being Function of A,REAL ;
take NORMSTR(# A,Z,a,M,n #) ; :: thesis: ( not NORMSTR(# A,Z,a,M,n #) is empty & NORMSTR(# A,Z,a,M,n #) is strict )
thus not the carrier of NORMSTR(# A,Z,a,M,n #) is empty ; :: according to STRUCT_0:def 1 :: thesis: NORMSTR(# A,Z,a,M,n #) is strict
thus NORMSTR(# A,Z,a,M,n #) is strict ; :: thesis: verum