let n be Ordinal; :: thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of n,L
for b being bag of n holds b *' (- p) = - (b *' p)
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Series of n,L
for b being bag of n holds b *' (- p) = - (b *' p)
let p be Series of n,L; :: thesis: for b being bag of n holds b *' (- p) = - (b *' p)
let b be bag of n; :: thesis: b *' (- p) = - (b *' p)
set q1 = b *' (- p);
set q2 = - (b *' p);
A1: now :: thesis: for x being object st x in dom (b *' (- p)) holds
(b *' (- p)) . x = (- (b *' p)) . x
let x be object ; :: thesis: ( x in dom (b *' (- p)) implies (b *' (- p)) . x = (- (b *' p)) . x )
assume x in dom (b *' (- p)) ; :: thesis: (b *' (- p)) . x = (- (b *' p)) . x
then reconsider u = x as bag of n ;
now :: thesis: ( ( b divides u & (b *' (- p)) . u = (- (b *' p)) . u ) or ( not b divides u & (b *' (- p)) . u = (- (b *' p)) . u ) )
per cases ( b divides u or not b divides u ) ;
case A2: b divides u ; :: thesis: (b *' (- p)) . u = (- (b *' p)) . u
then A3: (b *' p) . u = p . (u -' b) by POLYRED:def 1;
thus (b *' (- p)) . u = (- p) . (u -' b) by A2, POLYRED:def 1
.= - (p . (u -' b)) by POLYNOM1:17
.= (- (b *' p)) . u by A3, POLYNOM1:17 ; :: thesis: verum
end;
case A4: not b divides u ; :: thesis: (b *' (- p)) . u = (- (b *' p)) . u
then A5: (b *' p) . u = 0. L by POLYRED:def 1;
thus (b *' (- p)) . u = 0. L by A4, POLYRED:def 1
.= - (0. L) by RLVECT_1:12
.= (- (b *' p)) . u by A5, POLYNOM1:17 ; :: thesis: verum
end;
end;
end;
hence (b *' (- p)) . x = (- (b *' p)) . x ; :: thesis: verum
end;
dom (b *' (- p)) = Bags n by FUNCT_2:def 1
.= dom (- (b *' p)) by FUNCT_2:def 1 ;
hence b *' (- p) = - (b *' p) by A1, FUNCT_1:2; :: thesis: verum