let C be non empty set ; :: thesis: for V being non empty right_complementable add-associative right_zeroed addLoopStr
for f being PartFunc of C,V holds - (- f) = f
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for f being PartFunc of C,V holds - (- f) = f
let f be PartFunc of C,V; :: thesis: - (- f) = f
A1: dom (- (- f)) = dom (- f) by Def5;
A2: dom (- f) = dom f by Def5;

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

let c be Element of C; :: thesis: ( c in dom f implies (- (- f)) /. c = f /. c )
assume A3: c in dom f ; :: thesis: (- (- f)) /. c = f /. c
hence (- (- f)) /. c = - ((- f) /. c) by A1, A2, Def5
.= - (- (f /. c)) by A2, A3, Def5
.= f /. c ;
:: thesis: verum

end;

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