per cases ( not A is empty or A is empty ) ;

suppose A10: not A is empty ; :: thesis: for b₁, b₂ being Function of A,(QuotientOrder A) st ( for x being Element of A holds b₁ . x = Class ((EqRelOf A),x) ) & ( for x being Element of A holds b₂ . x = Class ((EqRelOf A),x) ) holds
b₁ = b₂

let f1, f2 be Function of A,(QuotientOrder A); :: thesis: ( ( for x being Element of A holds f1 . x = Class ((EqRelOf A),x) ) & ( for x being Element of A holds f2 . x = Class ((EqRelOf A),x) ) implies f1 = f2 )
assume that
A11: for x being Element of A holds f1 . x = Class ((EqRelOf A),x) and
A12: for x being Element of A holds f2 . x = Class ((EqRelOf A),x) ; :: thesis: f1 = f2
( dom f1 = the carrier of A & dom f2 = the carrier of A ) by A10, FUNCT_2:def 1;
then A13: dom f1 = dom f2 ;
for x being object st x in dom f1 holds
f1 . x = f2 . x

proof

let x be object ; :: thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume x in dom f1 ; :: thesis: f1 . x = f2 . x
then reconsider z = x as Element of A ;
( f1 . z = Class ((EqRelOf A),z) & f2 . z = Class ((EqRelOf A),z) ) by A11, A12;
hence f1 . x = f2 . x ; :: thesis: verum

end;

hence f1 = f2 by A13, FUNCT_1:2; :: thesis: verum

end;

suppose A is empty ; :: thesis: for b₁, b₂ being Function of A,(QuotientOrder A) st ( for x being Element of A holds b₁ . x = Class ((EqRelOf A),x) ) & ( for x being Element of A holds b₂ . x = Class ((EqRelOf A),x) ) holds
b₁ = b₂

then A14: QuotientOrder A is empty ;
let f1, f2 be Function of A,(QuotientOrder A); :: thesis: ( ( for x being Element of A holds f1 . x = Class ((EqRelOf A),x) ) & ( for x being Element of A holds f2 . x = Class ((EqRelOf A),x) ) implies f1 = f2 )
assume that
for x being Element of A holds f1 . x = Class ((EqRelOf A),x) and
for x being Element of A holds f2 . x = Class ((EqRelOf A),x) ; :: thesis: f1 = f2
thus f1 = f2 by A14; :: thesis: verum

end;

end;