let b be BinOp of INT ; :: thesis: ( b = multint iff for a, b being Element of INT holds b . a,b = multreal . a,b )

hereby :: thesis: ( ( for a, b being Element of INT holds b . a,b = multreal . a,b ) implies b = multint )

assume A1: b = multint ; :: thesis: for i1, i2 being Element of INT holds b . i1,i2 = multreal . i1,i2
let i1, i2 be Element of INT ; :: thesis: b . i1,i2 = multreal . i1,i2
A2: ( i1 in INT & i2 in INT ) ;
thus b . i1,i2 = i1 * i2 by A1, BINOP_2:def 22
.= multreal . i1,i2 by A2, BINOP_2:def 11, NUMBERS:15 ; :: thesis: verum

end;

assume A3: for i1, i2 being Element of INT holds b . i1,i2 = multreal . i1,i2 ; :: thesis: b = multint

now

let i1, i2 be Element of INT ; :: thesis: b . i1,i2 = multint . i1,i2
A4: ( i1 in INT & i2 in INT ) ;
thus b . i1,i2 = multreal . i1,i2 by A3
.= i1 * i2 by A4, BINOP_2:def 11, NUMBERS:15
.= multint . i1,i2 by BINOP_2:def 22 ; :: thesis: verum

end;

hence b = multint by BINOP_1:2; :: thesis: verum