deffunc H₁( Nat) -> Element of the carrier of S = (In (((p * (SgmX ((BagOrder n),(Support p)))) . $1),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. $1),x));
consider F being FinSequence of S such that
A1: len F = len (SgmX ((BagOrder n),(Support p))) and
A2: for n being Nat st n in dom F holds
F . n = H₁(n) from FINSEQ_2:sch 1();
take a = Sum F; :: thesis: ex y being FinSequence of S st
( a = 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)) ) )
take F ; :: thesis: ( a = Sum F & len F = len (SgmX ((BagOrder n),(Support p))) & ( for i being Element of NAT st 1 <= i & i <= len F holds
F . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) )
thus ( a = Sum F & len F = len (SgmX ((BagOrder n),(Support p))) ) by A1; :: thesis: for i being Element of NAT st 1 <= i & i <= len F holds
F . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x))

now :: thesis: for i being Element of NAT st 1 <= i & i <= len F holds
F . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x))

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len F implies F . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) )
assume ( 1 <= i & i <= len F ) ; :: thesis: F . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x))
then i in Seg (len F) ;
then i in dom F by FINSEQ_1:def 3;
hence F . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) by A2; :: thesis: verum

end;

hence for i being Element of NAT st 1 <= i & i <= len F holds
F . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ; :: thesis: verum