:: deftheorem Def11 defines (#) MATRIXJ1:def 11 :
for K being Field
for G1, G2, b₄ being FinSequence_of_Matrix of K holds
( b₄ = G1 (#) G2 iff ( dom b₄ = dom G1 & ( for i being Nat st i in dom b₄ holds
b₄ . i = (G1 . i) * (G2 . i) ) ) );