set S = SgmX ((BagOrder n),(Support p));
set l = len (SgmX ((BagOrder n),(Support p)));
defpred S₁[ 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 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 Nat st m in Seg (len (SgmX ((BagOrder n),(Support p)))) holds
S₁[m,q /. m] ) ) from RECDEF_1:sch 17(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;
for m being Element of NAT st 1 <= m & m <= len q holds
q /. m = ((p * (SgmX ((BagOrder n),(Support p)))) /. m) * (eval (((SgmX ((BagOrder n),(Support p))) /. m),x)) by A2, A3, FINSEQ_1:1;
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