for K being Field
for G1, G2 being FinSequence_of_Matrix of K holds
( Len (G1 (+) G2) = Len G1 & Width (G1 (+) G2) = Width G1 )