let n be set ; :: thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of n,L holds p = - (- p)
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Series of n,L holds p = - (- p)
let p be Series of n,L; :: thesis: p = - (- p)
set r = - p;
A2: dom p = Bags n by FUNCT_2:def 1;
A3: dom (- p) = Bags n by FUNCT_2:def 1;
A4: dom (- p) = dom p by VFUNCT_1:def 6;
A8: dom (- (- p)) = dom (- p) by VFUNCT_1:def 6;
A7: dom (- (- p)) = dom (- p) by VFUNCT_1:def 6;

now

let x be Element of Bags n; :: thesis: ( x in dom p implies p . x = (- (- p)) . x )
assume x in dom p ; :: thesis: p . x = (- (- p)) . x
A5: p . x = p /. x by A2, PARTFUN1:def 8;
thus p . x = - (- (p . x)) by RLVECT_1:30
.= - ((- p) /. x) by A2, A4, A5, VFUNCT_1:def 6
.= (- (- p)) /. x by A2, A4, A7, VFUNCT_1:def 6
.= (- (- p)) . x by A2, A4, A7, PARTFUN1:def 8 ; :: thesis: verum

end;

hence p = - (- p) by A2, A3, A8, PARTFUN1:34; :: thesis: verum