theorem :: MATGRP_0:62

for n being Nat
for L being non empty doubleLoopStr
for X, Y being Matrix of n,L
for x, y being Element of n -Matrices_over L st X = x & Y = y holds
X * Y = (matrix_mult (n,L)) . (x,y) by Def5;