theorem Th66: :: MATRIX_0:66

for D being non empty set
for G being Matrix of D
for i, n, m being Nat st i in Seg (width G) & width G > 1 & n in dom G & m in Seg (width (DelCol (G,i))) holds
(DelCol (G,i)) * (n,m) = (Del ((Line (G,n)),i)) . m