let IT, IT9 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 IT9 . (x,y) = x \/ y ) implies IT = IT9 )

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 IT9 . (x,y) = x \/ y ; :: thesis: IT = IT9

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 IT9 . (x,y) = x \/ y ; :: thesis: IT = IT9

now :: thesis: for x, y being Element of [:(Fin A),(Fin A):] holds IT . (x,y) = IT9 . (x,y)

hence
IT = IT9
; :: thesis: verumlet x, y be Element of [:(Fin A),(Fin A):]; :: thesis: IT . (x,y) = IT9 . (x,y)

thus IT . (x,y) = x \/ y by A1

.= IT9 . (x,y) by A2 ; :: thesis: verum

end;thus IT . (x,y) = x \/ y by A1

.= IT9 . (x,y) by A2 ; :: thesis: verum