let r, h be complex-valued Function; :: thesis: ( r = (- 1) (#) h implies h = (- 1) (#) r )
assume A1: r = (- 1) (#) h ; :: thesis: h = (- 1) (#) r
thus dom ((- 1) (#) r) = dom r by Def5
.= dom h by A1, Def5 ; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom h or h . b₁ = ((- 1) (#) r) . b₁ )
let c be object ; :: thesis: ( not c in dom h or h . c = ((- 1) (#) r) . c )
assume c in dom h ; :: thesis: h . c = ((- 1) (#) r) . c
reconsider a = (- 1) * (h . c) as Complex ;
thus h . c = (- 1) * a
.= (- 1) * (r . c) by A1, Th6
.= ((- 1) (#) r) . c by Th6 ; :: thesis: verum