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

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 :: thesis: for a, b being Element of [:(Fin A),(Fin A):] holds IT . (a,b) = IT9 . (a,b)

hence
IT = IT9
by BINOP_1:2; :: thesis: verumlet 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;IT . (a,b) = a \ b by A1;

hence IT . (a,b) = IT9 . (a,b) by A2; :: thesis: verum