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