deffunc H_{1}( Element of X) -> Element of Class E = EqClass (E,$1);

consider f being Function of X,(Class E) such that

A1: for x being Element of X holds f . x = H_{1}(x)
from FUNCT_2:sch 4();

take f ; :: thesis: for x being Element of X holds f . x = EqClass (E,x)

thus for x being Element of X holds f . x = EqClass (E,x) by A1; :: thesis: verum

consider f being Function of X,(Class E) such that

A1: for x being Element of X holds f . x = H

take f ; :: thesis: for x being Element of X holds f . x = EqClass (E,x)

thus for x being Element of X holds f . x = EqClass (E,x) by A1; :: thesis: verum