per cases ( not A is empty or A is empty ) ;
suppose A10: not A is empty ; :: thesis: for b1, b2 being Function of A,() st ( for x being Element of A holds b1 . x = Class ((),x) ) & ( for x being Element of A holds b2 . x = Class ((),x) ) holds
b1 = b2

let f1, f2 be Function of A,(); :: thesis: ( ( for x being Element of A holds f1 . x = Class ((),x) ) & ( for x being Element of A holds f2 . x = Class ((),x) ) implies f1 = f2 )
assume that
A11: for x being Element of A holds f1 . x = Class ((),x) and
A12: for x being Element of A holds f2 . x = Class ((),x) ; :: thesis: f1 = f2
( dom f1 = the carrier of A & dom f2 = the carrier of A ) by ;
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 ((),z) & f2 . z = Class ((),z) ) by ;
hence f1 . x = f2 . x ; :: thesis: verum
end;
hence f1 = f2 by ; :: thesis: verum
end;
suppose A is empty ; :: thesis: for b1, b2 being Function of A,() st ( for x being Element of A holds b1 . x = Class ((),x) ) & ( for x being Element of A holds b2 . x = Class ((),x) ) holds
b1 = b2

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