:: deftheorem defines F_Real VECTSP_1:def 5 :
F_Real = doubleLoopStr(# REAL,addreal,multreal,(In (1,REAL)),(In (0,REAL)) #);