deffunc H₁() -> set = {0,1,2};
deffunc H₂( object , object ) -> Element of H₁() = In ((IFEQ ($1,$2,$1,0)),H₁());
ex f being BinOp of H₁() st
for x, y being Element of H₁() holds f . (x,y) = H₂(x,y) from BINOP_1:sch 4();
then consider f being BinOp of H₁() such that
A1: for x, y being Element of H₁() holds f . (x,y) = H₂(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₁() by ENUMSET1:def 1;

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

assume A2: x = y ; :: thesis: f . (x,y) = x
thus f . (x,y) = H₂(x,y) by A1
.= In (x,H₁()) by A2, FUNCOP_1:def 8
.= x ; :: thesis: verum

end;

assume A3: x <> y ; :: thesis: f . (x,y) = 0
thus f . (x,y) = H₂(x,y) by A1
.= In (0,H₁()) by A3, FUNCOP_1:def 8
.= 0 by SUBSET_1:def 8, A4 ; :: thesis: verum