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