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
thus b . i = - i by A1, BINOP_2:def 19
.= compreal . i by BINOP_2:def 7 ; :: thesis: verum
end;
assume A2: for i being Element of INT holds b . i = compreal . i ; :: thesis: b = compint
now :: thesis: for i being Element of INT holds b . i = compint . i
let i be Element of INT ; :: thesis: b . i = compint . i
thus b . i = compreal . i by A2
.= - i by BINOP_2:def 7
.= compint . i by BINOP_2:def 19 ; :: thesis: verum
end;
hence b = compint by FUNCT_2:63; :: thesis: verum