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