for k, i, m, n being Nat
for D being non empty set
for M1 being Matrix of n,k,D
for M2 being Matrix of m,k,D st i in dom M1 holds
Line ((M1 ^ M2),i) = Line (M1,i)