:: deftheorem defines + PARSP_1:def 2 :
for F being Field
for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds x + y = (c3add F) . (x,y);