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