deffunc H1() -> set = {0,1,2};
deffunc H2( object , object ) -> Element of H1() = In ((IFEQ ($1,$2,$1,0)),H1());
ex f being BinOp of H1() st
for x, y being Element of H1() holds f . (x,y) = H2(x,y)
from BINOP_1:sch 4();
then consider f being BinOp of H1() such that
A1:
for x, y being Element of H1() holds f . (x,y) = H2(x,y)
;
take
f
; for x, y being Element of {0,1,2} holds
( ( x = y implies f . (x,y) = x ) & ( x <> y implies f . (x,y) = 0 ) )
let x, y be Element of {0,1,2}; ( ( x = y implies f . (x,y) = x ) & ( x <> y implies f . (x,y) = 0 ) )
A4:
0 in H1()
by ENUMSET1:def 1;
hereby ( x <> y implies f . (x,y) = 0 )
end;
assume A3:
x <> y
; f . (x,y) = 0
thus f . (x,y) =
H2(x,y)
by A1
.=
In (0,H1())
by A3, FUNCOP_1:def 8
.=
0
by SUBSET_1:def 8, A4
; verum