deffunc H₁( Element of {_{X}_}) -> Element of X = DeTrivial $1;
consider f being Function of {_{X}_},X such that
B1: for x being Element of {_{X}_} holds f . x = H₁(x) from FUNCT_2:sch 4();
take f ; :: thesis: for x being Element of {_{X}_} holds f . x = DeTrivial x
thus for x being Element of {_{X}_} holds f . x = DeTrivial x by B1; :: thesis: verum