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
A15: 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
A16: 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 :: thesis: for x being Element of C
for y being Element of Class R holds b1 . (x,y) = b2 . (x,y)

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 object such that
A17: y1 in D and
A18: y = Class (R,y1) by EQREL_1:def 3;
b1 . (x,y) = Class (R,(b . (x,y1))) by A15, A17, A18, EQREL_1:20;
hence b1 . (x,y) = b2 . (x,y) by A16, A17, A18, EQREL_1:20; :: thesis: verum

end;

hence b1 = b2 ; :: thesis: verum