:: deftheorem defines - PARSP_1:def 4 :
for F being Field
for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds - x = (c3compl F) . x;