let IT, IT' be BinOp of [:(Fin A),(Fin A):]; :: thesis: ( ( for x, y being Element of [:(Fin A),(Fin A):] holds IT . x,y = x \/ y ) & ( for x, y being Element of [:(Fin A),(Fin A):] holds IT' . x,y = x \/ y ) implies IT = IT' )
assume that
A1: for x, y being Element of [:(Fin A),(Fin A):] holds IT . x,y = x \/ y and
A2: for x, y being Element of [:(Fin A),(Fin A):] holds IT' . x,y = x \/ y ; :: thesis: IT = IT'

now

let x, y be Element of [:(Fin A),(Fin A):]; :: thesis: IT . x,y = IT' . x,y
thus IT . x,y = x \/ y by A1
.= IT' . x,y by A2 ; :: thesis: verum

end;

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