let IT, IT9 be BinOp of [:(Fin A),(Fin A):]; :: thesis: ( ( 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 ; :: thesis: IT = IT9

now

let a, b be Element of [:(Fin A),(Fin A):]; :: thesis: IT . a,b = IT9 . a,b
IT . a,b = a \ b by A1;
hence IT . a,b = IT9 . a,b by A2; :: thesis: verum

end;

hence IT = IT9 by BINOP_1:2; :: thesis: verum