set B = SgmX ((BagOrder X),(Support p));
deffunc H₁( object ) -> Element of K16(K17((Bags X), the carrier of L)) = (p . ((SgmX ((BagOrder X),(Support p))) /. $1)) * (Subst (((SgmX ((BagOrder X),(Support p))) /. $1),x,s));
consider S being FinSequence such that
A1: ( len S = len (SgmX ((BagOrder X),(Support p))) & ( for k being Nat st k in dom S holds
S . k = H₁(k) ) ) from FINSEQ_1:sch 2();
rng S c= the carrier of (Polynom-Ring (X,L))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng S or x in the carrier of (Polynom-Ring (X,L)) )
assume x in rng S ; :: thesis: x in the carrier of (Polynom-Ring (X,L))
then consider k being object such that
A2: ( k in dom S & S . k = x ) by FUNCT_1:def 3;
x = H₁(k) by A2, A1;
hence x in the carrier of (Polynom-Ring (X,L)) by POLYNOM1:def 11; :: thesis: verum

end;

then reconsider S = S as FinSequence of (Polynom-Ring (X,L)) by FINSEQ_1:def 4;
reconsider H = Sum S as Polynomial of X,L by POLYNOM1:def 11;
take H ; :: thesis: ex S being FinSequence of (Polynom-Ring (X,L)) st
( H = Sum S & len (SgmX ((BagOrder X),(Support p))) = len S & ( for i being Nat st i in dom S holds
S . i = (p . ((SgmX ((BagOrder X),(Support p))) /. i)) * (Subst (((SgmX ((BagOrder X),(Support p))) /. i),x,s)) ) )
take S ; :: thesis: ( H = Sum S & len (SgmX ((BagOrder X),(Support p))) = len S & ( for i being Nat st i in dom S holds
S . i = (p . ((SgmX ((BagOrder X),(Support p))) /. i)) * (Subst (((SgmX ((BagOrder X),(Support p))) /. i),x,s)) ) )
thus ( H = Sum S & len (SgmX ((BagOrder X),(Support p))) = len S & ( for i being Nat st i in dom S holds
S . i = (p . ((SgmX ((BagOrder X),(Support p))) /. i)) * (Subst (((SgmX ((BagOrder X),(Support p))) /. i),x,s)) ) ) by A1; :: thesis: verum