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
A6: 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
A7: 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
A8: len y1 = len (SgmX ((BagOrder n),(Support p))) and
A9: a = Sum y1 and
A10: 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 A6;
consider y2 being FinSequence of the carrier of L such that
A11: len y2 = len (SgmX ((BagOrder n),(Support p))) and
A12: c = Sum y2 and
A13: 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 A7;
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 that
A14: 1 <= k and
A15: k <= len y1 ; :: thesis: y1 . k = y2 . k
k in Seg (len y2) by A8, A11, A14, A15, FINSEQ_1:1;
then A16: k in dom y2 by FINSEQ_1:def 3;
A17: k in Seg (len y1) by A14, A15, FINSEQ_1:1;
then k in dom y1 by FINSEQ_1:def 3;
hence y1 . k = y1 /. k by PARTFUN1:def 6
.= ((p * (SgmX ((BagOrder n),(Support p)))) /. k) * (eval ((((SgmX ((BagOrder n),(Support p))) /. k) @),x)) by A10, A14, A15, A17
.= y2 /. k by A8, A11, A13, A14, A15, A17
.= y2 . k by A16, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence a = c by A8, A9, A11, A12, FINSEQ_1:14; :: thesis: verum