theorem Th6: :: VECTSP11:6

for i, n being Nat
for K being Field st i in Seg n holds
Delete ((1. (K,n)),i,i) = 1. (K,(n -' 1))