let f1, f2 be BinOp of {0,1,2}; ( ( for x, y being Element of {0,1,2} holds
( ( ( x = 1 or y = 1 ) implies f1 . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies f1 . (x,y) = min (x,y) ) ) ) & ( for x, y being Element of {0,1,2} holds
( ( ( x = 1 or y = 1 ) implies f2 . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies f2 . (x,y) = min (x,y) ) ) ) implies f1 = f2 )
assume that
A1:
for x, y being Element of {0,1,2} holds
( ( ( x = 1 or y = 1 ) implies f1 . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies f1 . (x,y) = min (x,y) ) )
and
A2:
for x, y being Element of {0,1,2} holds
( ( ( x = 1 or y = 1 ) implies f2 . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies f2 . (x,y) = min (x,y) ) )
; 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 = 1 or y = 1 or ( x <> 1 & y <> 1 ) )
;
suppose A3:
(
x = 1 or
y = 1 )
;
f1 . (x,y) = f2 . (x,y)then f1 . (
x,
y) =
1
by A1
.=
f2 . (
x,
y)
by A2, A3
;
hence
f1 . (
x,
y)
= f2 . (
x,
y)
;
verum end; suppose A3:
(
x <> 1 &
y <> 1 )
;
f1 . (x,y) = f2 . (x,y)then f1 . (
x,
y) =
min (
x,
y)
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