let b1, b2 be Function of [:C,(Class R):],(Class R); :: thesis: ( ( for x, y, y1 being set st x in C & y in Class R & y1 in y holds
b1 . (x,y) = Class (R,(b . (x,y1))) ) & ( for x, y, y1 being set st x in C & y in Class R & y1 in y holds
b2 . (x,y) = Class (R,(b . (x,y1))) ) implies b1 = b2 )
assume that
A18: for x, y, y1 being set st x in C & y in Class R & y1 in y holds
b1 . (x,y) = Class (R,(b . (x,y1))) and
A19: for x, y, y1 being set st x in C & y in Class R & y1 in y holds
b2 . (x,y) = Class (R,(b . (x,y1))) ; :: thesis: b1 = b2

now

let x be Element of C; :: thesis: for y being Element of Class R holds b1 . (x,y) = b2 . (x,y)
let y be Element of Class R; :: thesis: b1 . (x,y) = b2 . (x,y)
consider y1 being set such that
A22: y1 in D and
A23: y = Class (R,y1) by EQREL_1:def 3;
b1 . (x,y) = Class (R,(b . (x,y1))) by A18, A22, A23, EQREL_1:20;
hence b1 . (x,y) = b2 . (x,y) by A19, A22, A23, EQREL_1:20; :: thesis: verum

end;

hence b1 = b2 by BINOP_1:2; :: thesis: verum