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) & 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) & p + (- p) = 0_ (n,L) )
let p be Series of n,L; :: thesis: ( (- p) + p = 0_ (n,L) & p + (- p) = 0_ (n,L) )
set q = (- p) + p;
now :: thesis: for b being Element of Bags n holds ((- p) + p) . b = (0_ (n,L)) . b
let b be Element of Bags n; :: thesis: ((- p) + p) . b = (0_ (n,L)) . b
thus ((- p) + p) . b = ((- p) . b) + (p . b) by POLYNOM1:15
.= (- (p . b)) + (p . b) by POLYNOM1:17
.= 0. L by RLVECT_1:5
.= (0_ (n,L)) . b by POLYNOM1:22 ; :: thesis: verum
end;
hence (- p) + p = 0_ (n,L) by FUNCT_2:63; :: thesis: p + (- p) = 0_ (n,L)
set q = p + (- p);
now :: thesis: for b being Element of Bags n holds (p + (- p)) . b = (0_ (n,L)) . b
let b be Element of Bags n; :: thesis: (p + (- p)) . b = (0_ (n,L)) . b
thus (p + (- p)) . b = (p . b) + ((- p) . b) by POLYNOM1:15
.= (p . b) + (- (p . b)) by POLYNOM1:17
.= 0. L by RLVECT_1:5
.= (0_ (n,L)) . b by POLYNOM1:22 ; :: thesis: verum
end;
hence p + (- p) = 0_ (n,L) by FUNCT_2:63; :: thesis: verum