set S = SgmX (BagOrder n),(Support p);
set l = len (SgmX (BagOrder n),(Support p));
defpred S₁[ Element of NAT , Element of L] means $2 = ((p * (SgmX (BagOrder n),(Support p))) /. $1) * (eval (((SgmX (BagOrder n),(Support p)) /. $1) @ ),x);
A1: for k being Element of NAT st k in Seg (len (SgmX (BagOrder n),(Support p))) holds
ex x being Element of L st S₁[k,x] ;
consider q being FinSequence of the carrier of L such that
A2: ( dom q = Seg (len (SgmX (BagOrder n),(Support p))) & ( for m being Element of NAT st m in Seg (len (SgmX (BagOrder n),(Support p))) holds
S₁[m,q /. m] ) ) from POLYNOM2:sch 1(A1);
take Sum q ; :: thesis: ex y being FinSequence of the carrier of L st
( len y = len (SgmX (BagOrder n),(Support p)) & Sum q = 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) ) )
A3: len q = len (SgmX (BagOrder n),(Support p)) by A2, FINSEQ_1:def 3;

now

let m be Element of NAT ; :: thesis: ( 1 <= m & m <= len q implies q /. m = ((p * (SgmX (BagOrder n),(Support p))) /. m) * (eval (((SgmX (BagOrder n),(Support p)) /. m) @ ),x) )
assume that
A4: 1 <= m and
A5: m <= len q ; :: thesis: q /. m = ((p * (SgmX (BagOrder n),(Support p))) /. m) * (eval (((SgmX (BagOrder n),(Support p)) /. m) @ ),x)
m in Seg (len q) by A4, A5, FINSEQ_1:3;
hence q /. m = ((p * (SgmX (BagOrder n),(Support p))) /. m) * (eval (((SgmX (BagOrder n),(Support p)) /. m) @ ),x) by A2, A3; :: thesis: verum

end;

hence ex y being FinSequence of the carrier of L st
( len y = len (SgmX (BagOrder n),(Support p)) & Sum q = 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) ) ) by A3; :: thesis: verum