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 A2:
for i being Element of INT holds b . i = compreal . i
; :: thesis: 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;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

now :: thesis: for i being Element of INT holds b . i = compint . i

hence
b = compint
by FUNCT_2:63; :: thesis: verumlet 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;thus b . i = compreal . i by A2

.= - i by BINOP_2:def 7

.= compint . i by BINOP_2:def 19 ; :: thesis: verum