for F being Field
for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds - x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] by Def3;