consider D being non empty set , Z being Element of D, a being BinOp of D, m being Function of [:COMPLEX ,D:],D, s being Function of [:D,D:],COMPLEX ;
take CUNITSTR(# D,Z,a,m,s #) ; :: thesis: ( not CUNITSTR(# D,Z,a,m,s #) is empty & CUNITSTR(# D,Z,a,m,s #) is strict )
thus not the carrier of CUNITSTR(# D,Z,a,m,s #) is empty ; :: according to STRUCT_0:def 1 :: thesis: CUNITSTR(# D,Z,a,m,s #) is strict
thus CUNITSTR(# D,Z,a,m,s #) is strict ; :: thesis: verum