set D = the carrier of S \ { the OneF of S};
deffunc H₁( Element of the carrier of S \ { the OneF of S}) -> Element of INT = TrivialArity $1;
consider f being Function of ( the carrier of S \ { the OneF of S}),INT such that
A1: for x being Element of the carrier of S \ { the OneF of S} holds f . x = H₁(x) from FUNCT_2:sch 4();
take f ; :: thesis: for s being Element of the carrier of S \ { the OneF of S} holds f . s = TrivialArity s
thus for s being Element of the carrier of S \ { the OneF of S} holds f . s = TrivialArity s by A1; :: thesis: verum