let C be non empty set ; :: thesis: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-unital RLSStruct
for f being PartFunc of C,V holds - f = (- 1) (#) f
let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-unital RLSStruct ; :: thesis: for f being PartFunc of C,V holds - f = (- 1) (#) f
let f be PartFunc of C,V; :: thesis: - f = (- 1) (#) f
A1: dom (- f) = dom f by Def5
.= dom ((- 1) (#) f) by Def4 ;

now :: thesis: for c being Element of C st c in dom ((- 1) (#) f) holds
(- f) /. c = ((- 1) (#) f) /. c

let c be Element of C; :: thesis: ( c in dom ((- 1) (#) f) implies (- f) /. c = ((- 1) (#) f) /. c )
assume A2: c in dom ((- 1) (#) f) ; :: thesis: (- f) /. c = ((- 1) (#) f) /. c
hence (- f) /. c = - (f /. c) by A1, Def5
.= (- 1) * (f /. c) by RLVECT_1:16
.= ((- 1) (#) f) /. c by A2, Def4 ;
:: thesis: verum

end;

hence - f = (- 1) (#) f by A1, PARTFUN2:1; :: thesis: verum