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

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

let b be Element of Bags n; :: thesis: pp . b = p . b
thus pp . b = (p + (- (0_ (n,L)))) . b by POLYNOM1:def 7
.= (p . b) + ((- (0_ (n,L))) . b) by POLYNOM1:15
.= (p . b) + (- ((0_ (n,L)) . b)) by POLYNOM1:17
.= (p . b) + (- (0. L)) by POLYNOM1:22
.= (p . b) - (0. L)
.= p . b by RLVECT_1:13 ; :: thesis: verum

end;

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