deffunc H1( Subset of R, Subset of R) -> set = 1 - (JaccardIndex ($1,$2));
let f1, f2 be Function of [:(bool R),(bool R):],REAL; ( ( for A, B being Subset of R holds f1 . (A,B) = 1 - (JaccardIndex (A,B)) ) & ( for A, B being Subset of R holds f2 . (A,B) = 1 - (JaccardIndex (A,B)) ) implies f1 = f2 )
assume that
A1:
for x, y being Subset of R holds f1 . (x,y) = H1(x,y)
and
A2:
for x, y being Subset of R holds f2 . (x,y) = H1(x,y)
; f1 = f2
for x, y being Subset of R holds f1 . (x,y) = f2 . (x,y)
proof
let x,
y be
Subset of
R;
f1 . (x,y) = f2 . (x,y)
f1 . (
x,
y) =
H1(
x,
y)
by A1
.=
f2 . (
x,
y)
by A2
;
hence
f1 . (
x,
y)
= f2 . (
x,
y)
;
verum
end;
hence
f1 = f2
by BINOP_1:2; verum