deffunc H₁( Element of Permutations n) -> Element of the carrier of K = the multF of K $$ (Path_matrix $1,M);
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)
thus for p being Element of Permutations n holds f . p = the multF of K $$ (Path_matrix p,M) by A1; :: thesis: verum