let n be set ; :: thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p, r being Series of n,L st ( for x being bag of n holds r . x = - (p . x) ) holds
r = - p
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p, r being Series of n,L st ( for x being bag of n holds r . x = - (p . x) ) holds
r = - p
let p, r be Series of n,L; :: thesis: ( ( for x being bag of n holds r . x = - (p . x) ) implies r = - p )
assume A1: for x being bag of n holds r . x = - (p . x) ; :: thesis: r = - p
let x be Element of Bags n; :: according to FUNCT_2:def 8 :: thesis: r . x = (- p) . x
A2: dom (- p) = Bags n by FUNCT_2:def 1;
A3: (- p) /. x = (- p) . x ;
A5: p /. x = p . x ;
thus r . x = - (p . x) by A1
.= (- p) . x by A2, A3, A5, VFUNCT_1:def 5 ; :: thesis: verum