theorem Th18: :: MATRIX15:18

for i, k, m, n being Nat
for D being non empty set
for A being Matrix of n,m,D
for B being Matrix of n,k,D
for pA, pB being FinSequence of D st len pA = width A & len pB = width B holds
ReplaceLine ((A ^^ B),i,(pA ^ pB)) = (ReplaceLine (A,i,pA)) ^^ (ReplaceLine (B,i,pB))