let y1, y2 be Element of S; :: thesis: ( ex y being FinSequence of S st
( y1 = Sum y & len y = len (SgmX ((BagOrder n),(Support p))) & ( for i being Element of NAT st 1 <= i & i <= len y holds
y . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) ) & ex y being FinSequence of S st
( y2 = Sum y & len y = len (SgmX ((BagOrder n),(Support p))) & ( for i being Element of NAT st 1 <= i & i <= len y holds
y . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) ) implies y1 = y2 )
assume that
A1: ex F1 being FinSequence of S st
( y1 = Sum F1 & len F1 = len (SgmX ((BagOrder n),(Support p))) & ( for i being Element of NAT st 1 <= i & i <= len F1 holds
F1 . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) ) and
A2: ex F2 being FinSequence of S st
( y2 = Sum F2 & len F2 = len (SgmX ((BagOrder n),(Support p))) & ( for i being Element of NAT st 1 <= i & i <= len F2 holds
F2 . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) ) ; :: thesis: y1 = y2
consider F1 being FinSequence of S such that
A3: y1 = Sum F1 and
A4: len F1 = len (SgmX ((BagOrder n),(Support p))) and
A5: for i being Element of NAT st 1 <= i & i <= len F1 holds
F1 . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) by A1;
consider F2 being FinSequence of S such that
A6: y2 = Sum F2 and
A7: len F2 = len (SgmX ((BagOrder n),(Support p))) and
A8: for i being Element of NAT st 1 <= i & i <= len F2 holds
F2 . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) by A2;
A9: dom F1 = Seg (len F2) by A4, A7, FINSEQ_1:def 3;

now :: thesis: for i being Nat st i in dom F1 holds
F1 . i = F2 . i

let i be Nat; :: thesis: ( i in dom F1 implies F1 . i = F2 . i )
A13: i is Element of NAT by ORDINAL1:def 12;
assume A10: i in dom F1 ; :: thesis: F1 . i = F2 . i
then i in Seg (len F1) by FINSEQ_1:def 3;
then A14: ( 1 <= i & i <= len F1 ) by FINSEQ_1:1;
A15: ( 1 <= i & i <= len F2 ) by A10, A9, FINSEQ_1:1;
thus F1 . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) by A5, A14, A13
.= F2 . i by A8, A15, A13 ; :: thesis: verum

end;

hence y1 = y2 by A3, A4, A6, A7, FINSEQ_2:9; :: thesis: verum