for K being Field
for G, G9, G1, G2 being FinSequence_of_Matrix of K st len G = len G9 holds
(G ^ G1) (+) (G9 ^ G2) = (G (+) G9) ^ (G1 (+) G2)