let f1, f2 be BinOp of {0,1,2}; ( ( for x, y being Element of {0,1,2} holds
( ( x = y implies f1 . (x,y) = x ) & ( x <> y implies f1 . (x,y) = 0 ) ) ) & ( for x, y being Element of {0,1,2} holds
( ( x = y implies f2 . (x,y) = x ) & ( x <> y implies f2 . (x,y) = 0 ) ) ) implies f1 = f2 )
assume that
A1:
for x, y being Element of {0,1,2} holds
( ( x = y implies f1 . (x,y) = x ) & ( x <> y implies f1 . (x,y) = 0 ) )
and
A2:
for x, y being Element of {0,1,2} holds
( ( x = y implies f2 . (x,y) = x ) & ( x <> y implies f2 . (x,y) = 0 ) )
; f1 = f2
for x, y being Element of {0,1,2} holds f1 . (x,y) = f2 . (x,y)
proof
let x,
y be
Element of
{0,1,2};
f1 . (x,y) = f2 . (x,y)
per cases
( x = y or x <> y )
;
suppose A3:
x = y
;
f1 . (x,y) = f2 . (x,y)then f1 . (
x,
y) =
x
by A1
.=
f2 . (
x,
y)
by A2, A3
;
hence
f1 . (
x,
y)
= f2 . (
x,
y)
;
verum end; suppose A3:
x <> y
;
f1 . (x,y) = f2 . (x,y)then f1 . (
x,
y) =
0
by A1
.=
f2 . (
x,
y)
by A2, A3
;
hence
f1 . (
x,
y)
= f2 . (
x,
y)
;
verum end; end;
end;
hence
f1 = f2
by BINOP_1:2; verum