theorem :: MATRLIN2:37

for K being Field
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for A, B being Matrix of len b1, len B2,K holds Mx2Tran ((A + B),b1,B2) = (Mx2Tran (A,b1,B2)) + (Mx2Tran (B,b1,B2))