:: deftheorem defines multEX_0 ALGSTR_1:def 7 :
multEX_0 = multLoopStr_0(# REAL,multreal,(In (0,REAL)),(In (1,REAL)) #);