let IT1, IT2 be Function of X,(Class E); :: thesis: ( ( for x being Element of X holds IT1 . x = EqClass (E,x) ) & ( for x being Element of X holds IT2 . x = EqClass (E,x) ) implies IT1 = IT2 )
assume A2: for x being Element of X holds IT1 . x = EqClass (E,x) ; :: thesis: ( ex x being Element of X st not IT2 . x = EqClass (E,x) or IT1 = IT2 )
assume A3: for x being Element of X holds IT2 . x = EqClass (E,x) ; :: thesis: IT1 = IT2

now :: thesis: for x being Element of X holds IT1 . x = IT2 . x

let x be Element of X; :: thesis: IT1 . x = IT2 . x
thus IT1 . x = EqClass (E,x) by A2
.= IT2 . x by A3 ; :: thesis: verum

end;

hence IT1 = IT2 by FUNCT_2:63; :: thesis: verum