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