let n be set ; :: thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of n,L
for x being bag of n holds (- p) . x = - (p . x)
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Series of n,L
for x being bag of n holds (- p) . x = - (p . x)
let p be Series of n,L; :: thesis: for x being bag of n holds (- p) . x = - (p . x)
let x be bag of n; :: thesis: (- p) . x = - (p . x)
A1: dom p = Bags n by FUNCT_2:def 1;
A2: x in Bags n by PRE_POLY:def 12;
then A3: p /. x = p . x by A1, PARTFUN1:def 6;
A4: dom (- p) = dom p by VFUNCT_1:def 5;
hence (- p) . x = (- p) /. x by A1, A2, PARTFUN1:def 6
.= - (p . x) by A1, A2, A3, A4, VFUNCT_1:def 5 ;
:: thesis: verum