theorem :: MATRIX_0:75

for i, n being Nat
for D being non empty set
for m being Nat
for f being FinSequence of D
for G being Matrix of D st rng f misses rng (Col (G,i)) & f /. n in rng (Line (G,m)) & n in dom f & i in Seg (width G) & m in dom G & width G > 1 holds
f /. n in rng (Line ((DelCol (G,i)),m))