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 A2:
for i1, i2 being Element of INT holds b . (i1,i2) = multreal . (i1,i2)
; :: thesis: 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)

thus b . (i1,i2) = i1 * i2 by A1, BINOP_2:def 22

.= multreal . (i1,i2) by BINOP_2:def 11 ; :: thesis: verum

end;let i1, i2 be Element of INT ; :: thesis: b . (i1,i2) = multreal . (i1,i2)

thus b . (i1,i2) = i1 * i2 by A1, BINOP_2:def 22

.= multreal . (i1,i2) by BINOP_2:def 11 ; :: thesis: verum

now :: thesis: for i1, i2 being Element of INT holds b . (i1,i2) = multint . (i1,i2)

hence
b = multint
by BINOP_1:2; :: thesis: verumlet i1, i2 be Element of INT ; :: thesis: b . (i1,i2) = multint . (i1,i2)

thus b . (i1,i2) = multreal . (i1,i2) by A2

.= i1 * i2 by BINOP_2:def 11

.= multint . (i1,i2) by BINOP_2:def 22 ; :: thesis: verum

end;thus b . (i1,i2) = multreal . (i1,i2) by A2

.= i1 * i2 by BINOP_2:def 11

.= multint . (i1,i2) by BINOP_2:def 22 ; :: thesis: verum