let b be BinOp of INT; :: thesis: ( b = addint iff for i1, i2 being Element of INT holds b . (i1,i2) = addreal . (i1,i2) )
hereby :: thesis: ( ( for i1, i2 being Element of INT holds b . (i1,i2) = addreal . (i1,i2) ) implies b = addint )
assume A1: b = addint ; :: thesis: for i1, i2 being Element of INT holds b . (i1,i2) = addreal . (i1,i2)
let i1, i2 be Element of INT ; :: thesis: b . (i1,i2) = addreal . (i1,i2)
thus b . (i1,i2) = i1 + i2 by A1, BINOP_2:def 20
.= addreal . (i1,i2) by BINOP_2:def 9 ; :: thesis: verum
end;
assume A2: for i1, i2 being Element of INT holds b . (i1,i2) = addreal . (i1,i2) ; :: thesis: b = addint
now :: thesis: for i1, i2 being Element of INT holds b . (i1,i2) = addint . (i1,i2)
let i1, i2 be Element of INT ; :: thesis: b . (i1,i2) = addint . (i1,i2)
thus b . (i1,i2) = addreal . (i1,i2) by A2
.= i1 + i2 by BINOP_2:def 9
.= addint . (i1,i2) by BINOP_2:def 20 ; :: thesis: verum
end;
hence b = addint ; :: thesis: verum