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 [:REAL, the non empty set :], the non empty set ;
set s = the Function of [: the non empty set , the non empty set :],REAL;
take
UNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],REAL #)
; ( not UNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is empty & UNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is strict )
thus
not the carrier of UNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is empty
; STRUCT_0:def 1 UNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is strict
thus
UNITSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :],REAL #) is strict
; verum