let a1, a2 be Series of n,F_Real; :: thesis: ( ( for b being bag of n holds a1 . b = |.(p . b).| ) & ( for b being bag of n holds a2 . b = |.(p . b).| ) implies a1 = a2 )
assume that
A3: for b being bag of n holds a1 . b = |.(p . b).| and
A4: for b being bag of n holds a2 . b = |.(p . b).| ; :: thesis: a1 = a2
now :: thesis: for x being Element of Bags n holds a1 . x = a2 . x
let x be Element of Bags n; :: thesis: a1 . x = a2 . x
thus a1 . x = |.(p . x).| by A3
.= a2 . x by A4 ; :: thesis: verum
end;
hence a1 = a2 ; :: thesis: verum