set B = SgmX ((BagOrder X),(Support p));
let P1, P2 be Polynomial of X,L; :: thesis: ( ex S being FinSequence of (Polynom-Ring (X,L)) st
( P1 = 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)) ) ) & ex S being FinSequence of (Polynom-Ring (X,L)) st
( P2 = 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)) ) ) implies P1 = P2 )
given S1 being FinSequence of (Polynom-Ring (X,L)) such that A3: ( P1 = Sum S1 & len (SgmX ((BagOrder X),(Support p))) = len S1 & ( for i being Nat st i in dom S1 holds
S1 . i = (p . ((SgmX ((BagOrder X),(Support p))) /. i)) * (Subst (((SgmX ((BagOrder X),(Support p))) /. i),x,s)) ) ) ; :: thesis: ( for S being FinSequence of (Polynom-Ring (X,L)) holds
( not P2 = Sum S or not len (SgmX ((BagOrder X),(Support p))) = len S or ex i being Nat st
( i in dom S & not S . i = (p . ((SgmX ((BagOrder X),(Support p))) /. i)) * (Subst (((SgmX ((BagOrder X),(Support p))) /. i),x,s)) ) ) or P1 = P2 )
given S2 being FinSequence of (Polynom-Ring (X,L)) such that A4: ( P2 = Sum S2 & len (SgmX ((BagOrder X),(Support p))) = len S2 & ( for i being Nat st i in dom S2 holds
S2 . i = (p . ((SgmX ((BagOrder X),(Support p))) /. i)) * (Subst (((SgmX ((BagOrder X),(Support p))) /. i),x,s)) ) ) ; :: thesis: P1 = P2
A5: dom S1 = dom S2 by A3, A4, FINSEQ_3:29;
for i being Nat st i in dom S1 holds
S1 . i = S2 . i

proof

let i be Nat; :: thesis: ( i in dom S1 implies S1 . i = S2 . i )
assume A6: i in dom S1 ; :: thesis: S1 . i = S2 . i
( S1 . i = (p . ((SgmX ((BagOrder X),(Support p))) /. i)) * (Subst (((SgmX ((BagOrder X),(Support p))) /. i),x,s)) & (p . ((SgmX ((BagOrder X),(Support p))) /. i)) * (Subst (((SgmX ((BagOrder X),(Support p))) /. i),x,s)) = S2 . i ) by A6, A3, A4, A5;
hence S1 . i = S2 . i ; :: thesis: verum

end;

hence P1 = P2 by A3, A4, FINSEQ_3:29, FINSEQ_1:13; :: thesis: verum