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 = 0_ (n,L)
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Series of n,L holds p - p = 0_ (n,L)
let p be Series of n,L; :: thesis: p - p = 0_ (n,L)
reconsider pp = p - p, Z = 0_ (n,L) as Function of (Bags n), the carrier of L ;

now :: thesis: for b being Element of Bags n holds pp . b = Z . b

let b be Element of Bags n; :: thesis: pp . b = Z . b
thus pp . b = (p . b) + ((- p) . b) by Th15
.= (p . b) + (- (p . b)) by Th17
.= 0. L by RLVECT_1:def 10
.= Z . b ; :: thesis: verum

end;

hence p - p = 0_ (n,L) ; :: thesis: verum