deffunc H_{1}( 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_{1}(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

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

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