:: deftheorem Def10 defines (+) MATRIXJ1:def 10 :
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) ) ) );