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

end;

suppose A10:
not A is empty
; :: thesis: for b_{1}, b_{2} being Function of A,(QuotientOrder A) st ( for x being Element of A holds b_{1} . x = Class ((EqRelOf A),x) ) & ( for x being Element of A holds b_{2} . x = Class ((EqRelOf A),x) ) holds

b_{1} = b_{2}

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

end;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

hence
f1 = f2
by A13, FUNCT_1:2; :: thesis: verum
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;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

suppose
A is empty
; :: thesis: for b_{1}, b_{2} being Function of A,(QuotientOrder A) st ( for x being Element of A holds b_{1} . x = Class ((EqRelOf A),x) ) & ( for x being Element of A holds b_{2} . x = Class ((EqRelOf A),x) ) holds

b_{1} = b_{2}

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;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