deffunc H₁( Element of Permutations n) -> Element of the carrier of K = - (the multF of K $$ (Path_matrix $1,M)),$1;
consider f being Function of (Permutations n),the carrier of K such that
A1: for p being Element of Permutations n holds f . p = H₁(p) from FUNCT_2:sch 4();
take f ; :: thesis: for p being Element of Permutations n holds f . p = - (the multF of K $$ (Path_matrix p,M)),p
thus for p being Element of Permutations n holds f . p = - (the multF of K $$ (Path_matrix p,M)),p by A1; :: thesis: verum