for F being Field
for a, b, c, d being Element of (MPS F) holds [[a,b],[c,d]] in 4C_3 F ;