let f1, f2 be BinOp of T; ( ( for a, b being Element of T holds f1 . (a,b) = Tern (a,x,b) ) & ( for a, b being Element of T holds f2 . (a,b) = Tern (a,x,b) ) implies f1 = f2 )
assume that
A1:
for a, b being Element of T holds f1 . (a,b) = Tern (a,x,b)
and
A2:
for a, b being Element of T holds f2 . (a,b) = Tern (a,x,b)
; f1 = f2
for a, b being Element of T holds f1 . (a,b) = f2 . (a,b)
proof
let a,
b be
Element of
T;
f1 . (a,b) = f2 . (a,b)
f1 . (
a,
b) =
Tern (
a,
x,
b)
by A1
.=
f2 . (
a,
b)
by A2
;
hence
f1 . (
a,
b)
= f2 . (
a,
b)
;
verum
end;
hence
f1 = f2
by BINOP_1:2; verum