let f1, f2 be BinOp of (Carrier f); :: thesis: ( ( for a, b being Element of Carrier f ex i being Element of NAT ex x, y being Element of (f . i) st
( x = a & y = b & f1 . (a,b) = x + y ) ) & ( for a, b being Element of Carrier f ex i being Element of NAT ex x, y being Element of (f . i) st
( x = a & y = b & f2 . (a,b) = x + y ) ) implies f1 = f2 )
assume that
A1: for a, b being Element of Carrier f ex i being Element of NAT ex x, y being Element of (f . i) st
( x = a & y = b & f1 . (a,b) = x + y ) and
A2: for a, b being Element of Carrier f ex i being Element of NAT ex x, y being Element of (f . i) st
( x = a & y = b & f2 . (a,b) = x + y ) ; :: thesis: f1 = f2

now :: thesis: for a, b being Element of Carrier f holds f1 . (a,b) = f2 . (a,b)

let a, b be Element of Carrier f; :: thesis: f1 . (a,b) = f2 . (a,b)
consider i being Element of NAT , xi, yi being Element of (f . i) such that
A3: ( xi = a & yi = b & f1 . (a,b) = xi + yi ) by A1;
consider j being Element of NAT , xj, yj being Element of (f . j) such that
A4: ( xj = a & yj = b & f2 . (a,b) = xj + yj ) by A2;
thus f1 . (a,b) = f2 . (a,b) by A3, A4, lem2; :: thesis: verum

end;

hence f1 = f2 ; :: thesis: verum