deffunc H1( Subset of R, Subset of R) -> set = ((CMap (kappa_2 R)) . ($1,$2)) + ((CMap (kappa_2 R)) . ($2,$1));
let f1, f2 be preRIF of R; ( ( for x, y being Subset of R holds f1 . (x,y) = ((CMap (kappa_2 R)) . (x,y)) + ((CMap (kappa_2 R)) . (y,x)) ) & ( for x, y being Subset of R holds f2 . (x,y) = ((CMap (kappa_2 R)) . (x,y)) + ((CMap (kappa_2 R)) . (y,x)) ) 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