for n being Nat
for K being Fanoian Field
for p2 being Element of Permutations (n + 2)
for X, Y being Element of Fin (2Set (Seg (n + 2))) st Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) } holds
the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(card Y))