:: deftheorem defines G_Real VECTSP_1:def 1 :
G_Real = addLoopStr(# REAL,addreal,(In (0,REAL)) #);