theorem Th4: :: MATRIX11:4

for n being Nat
for K being commutative Ring
for p2 being Element of Permutations (n + 2)
for X being Element of Fin (2Set (Seg (n + 2))) st ( for x being object st x in X holds
(Part_sgn (p2,K)) . x = 1_ K ) holds
the multF of K $$ (X,(Part_sgn (p2,K))) = 1_ K