let b be UnOp of INT ; :: thesis: ( b = compint iff for a being Element of INT holds b . a = compreal . a )

hereby :: thesis: ( ( for a being Element of INT holds b . a = compreal . a ) implies b = compint )

assume A1: b = compint ; :: thesis: for i being Element of INT holds b . i = compreal . i
let i be Element of INT ; :: thesis: b . i = compreal . i
A2: i in INT ;
thus b . i = - i by A1, BINOP_2:def 19
.= compreal . i by A2, BINOP_2:def 7, NUMBERS:15 ; :: thesis: verum

end;

assume A3: for i being Element of INT holds b . i = compreal . i ; :: thesis: b = compint

now

let i be Element of INT ; :: thesis: b . i = compint . i
A4: i in INT ;
thus b . i = compreal . i by A3
.= - i by A4, BINOP_2:def 7, NUMBERS:15
.= compint . i by BINOP_2:def 19 ; :: thesis: verum

end;

hence b = compint by FUNCT_2:113; :: thesis: verum