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;
A1: dom p = Bags n by FUNCT_2:def 1;
A2: dom (- p) = dom p by VFUNCT_1:def 5;
A3: dom (- (- p)) = dom (- p) by VFUNCT_1:def 5;

now :: thesis: for x being Element of Bags n st x in dom p holds
p . x = (- (- p)) . x

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
A4: p . x = p /. x ;
thus p . x = - (- (p . x)) by RLVECT_1:17
.= - ((- p) /. x) by A1, A2, A4, VFUNCT_1:def 5
.= (- (- p)) /. x by A1, A2, A3, VFUNCT_1:def 5
.= (- (- p)) . x ; :: thesis: verum

end;

hence p = - (- p) by A1; :: thesis: verum