:: deftheorem defines @" MATRIXC1:def 2 :
for M being Matrix of COMPLEX holds M @" = (M @) *' ;