let b1, b2 be Function of [:C,(Class R):],(Class R); ( ( 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)))
; b1 = b2
now 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;
for y being Element of Class R holds b1 . (x,y) = b2 . (x,y)let y be
Element of
Class R;
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;
verum end;
hence
b1 = b2
; verum