let a, c be Element of L; :: thesis: ( ex y being FinSequence of the carrier of L st
( len y = len (SgmX (BagOrder n),(Support p)) & a = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX (BagOrder n),(Support p))) /. i) * (eval (((SgmX (BagOrder n),(Support p)) /. i) @ ),x) ) ) & ex y being FinSequence of the carrier of L st
( len y = len (SgmX (BagOrder n),(Support p)) & c = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX (BagOrder n),(Support p))) /. i) * (eval (((SgmX (BagOrder n),(Support p)) /. i) @ ),x) ) ) implies a = c )
assume that
A4: ex y1 being FinSequence of the carrier of L st
( len y1 = len (SgmX (BagOrder n),(Support p)) & a = Sum y1 & ( for i being Element of NAT st 1 <= i & i <= len y1 holds
y1 /. i = ((p * (SgmX (BagOrder n),(Support p))) /. i) * (eval (((SgmX (BagOrder n),(Support p)) /. i) @ ),x) ) ) and
A5: ex y2 being FinSequence of the carrier of L st
( len y2 = len (SgmX (BagOrder n),(Support p)) & c = Sum y2 & ( for i being Element of NAT st 1 <= i & i <= len y2 holds
y2 /. i = ((p * (SgmX (BagOrder n),(Support p))) /. i) * (eval (((SgmX (BagOrder n),(Support p)) /. i) @ ),x) ) ) ; :: thesis: a = c
consider y1 being FinSequence of the carrier of L such that
A6: ( len y1 = len (SgmX (BagOrder n),(Support p)) & a = Sum y1 & ( for i being Element of NAT st 1 <= i & i <= len y1 holds
y1 /. i = ((p * (SgmX (BagOrder n),(Support p))) /. i) * (eval (((SgmX (BagOrder n),(Support p)) /. i) @ ),x) ) ) by A4;
consider y2 being FinSequence of the carrier of L such that
A7: ( len y2 = len (SgmX (BagOrder n),(Support p)) & c = Sum y2 & ( for i being Element of NAT st 1 <= i & i <= len y2 holds
y2 /. i = ((p * (SgmX (BagOrder n),(Support p))) /. i) * (eval (((SgmX (BagOrder n),(Support p)) /. i) @ ),x) ) ) by A5;
for k being Nat st 1 <= k & k <= len y1 holds
y1 . k = y2 . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len y1 implies y1 . k = y2 . k )
assume A8: ( 1 <= k & k <= len y1 ) ; :: thesis: y1 . k = y2 . k
then A9: ( k in Seg (len y1) & k in Seg (len y2) ) by A6, A7, FINSEQ_1:3;
then A10: ( k in dom y1 & k in dom y2 ) by FINSEQ_1:def 3;
hence y1 . k = y1 /. k by PARTFUN1:def 8
.= ((p * (SgmX (BagOrder n),(Support p))) /. k) * (eval (((SgmX (BagOrder n),(Support p)) /. k) @ ),x) by A6, A8, A9
.= y2 /. k by A6, A7, A8, A9
.= y2 . k by A10, PARTFUN1:def 8 ;
:: thesis: verum

end;

hence a = c by A6, A7, FINSEQ_1:18; :: thesis: verum