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