set A = 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 n = the Function of the non empty set ,REAL;
take NORMSTR(# 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 ,REAL #) ; :: thesis: ( not NORMSTR(# 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 ,REAL #) is empty & NORMSTR(# 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 ,REAL #) is strict )
thus not the carrier of NORMSTR(# 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 ,REAL #) is empty ; :: according to STRUCT_0:def 1 :: thesis: NORMSTR(# 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 ,REAL #) is strict
thus NORMSTR(# 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 ,REAL #) is strict ; :: thesis: verum