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

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

hence
a1 = a2
; :: thesis: verumlet 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;thus a1 . x = |.(p . x).| by A3

.= a2 . x by A4 ; :: thesis: verum