let IT, IT9 be BinOp of [:(Fin A),(Fin A):]; ( ( for a, b being Element of [:(Fin A),(Fin A):] holds IT . (a,b) = a \ b ) & ( for a, b being Element of [:(Fin A),(Fin A):] holds IT9 . (a,b) = a \ b ) implies IT = IT9 )
assume that
A1:
for a, b being Element of [:(Fin A),(Fin A):] holds IT . (a,b) = a \ b
and
A2:
for a, b being Element of [:(Fin A),(Fin A):] holds IT9 . (a,b) = a \ b
; IT = IT9
hence
IT = IT9
by BINOP_1:2; verum