deffunc H_{1}() -> set = {0,1,2};

deffunc H_{2}( object , object ) -> Element of H_{1}() = In ((IFEQ ($1,$2,$1,0)),H_{1}());

ex f being BinOp of H_{1}() st

for x, y being Element of H_{1}() holds f . (x,y) = H_{2}(x,y)
from BINOP_1:sch 4();

then consider f being BinOp of H_{1}() such that

A1: for x, y being Element of H_{1}() holds f . (x,y) = H_{2}(x,y)
;

take f ; :: thesis: 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}; :: thesis: ( ( x = y implies f . (x,y) = x ) & ( x <> y implies f . (x,y) = 0 ) )

A4: 0 in H_{1}()
by ENUMSET1:def 1;

thus f . (x,y) = H_{2}(x,y)
by A1

.= In (0,H_{1}())
by A3, FUNCOP_1:def 8

.= 0 by SUBSET_1:def 8, A4 ; :: thesis: verum

deffunc H

ex f being BinOp of H

for x, y being Element of H

then consider f being BinOp of H

A1: for x, y being Element of H

take f ; :: thesis: 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}; :: thesis: ( ( x = y implies f . (x,y) = x ) & ( x <> y implies f . (x,y) = 0 ) )

A4: 0 in H

hereby :: thesis: ( x <> y implies f . (x,y) = 0 )

assume A3:
x <> y
; :: thesis: f . (x,y) = 0 assume A2:
x = y
; :: thesis: f . (x,y) = x

thus f . (x,y) = H_{2}(x,y)
by A1

.= In (x,H_{1}())
by A2, FUNCOP_1:def 8

.= x ; :: thesis: verum

end;thus f . (x,y) = H

.= In (x,H

.= x ; :: thesis: verum

thus f . (x,y) = H

.= In (0,H

.= 0 by SUBSET_1:def 8, A4 ; :: thesis: verum