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