set D = the non empty set ;
set Z = the Element of the non empty set ;
set a = the BinOp of the non empty set ;
set m = the Function of [:COMPLEX, the non empty set :], the non empty set ;
set s = the Function of [: the non empty set , the non empty set :],COMPLEX;
take
CUNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],COMPLEX #)
; ( not CUNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],COMPLEX #) is empty & CUNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],COMPLEX #) is strict )
thus
( not CUNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],COMPLEX #) is empty & CUNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],COMPLEX #) is strict )
; verum