set C = nMatrixFieldCat (K,o,n);
for f, g being Morphism of (nMatrixFieldCat (K,o,n)) st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) ;
hence nMatrixFieldCat (K,o,n) is transitive by CAT_1:def 7; :: thesis: verum