set S = SgmX (RelIncl n),(support b);
set l = len (SgmX (RelIncl n),(support b));
defpred S₁[ Element of NAT , Element of L] means $2 = (power L) . ((x * (SgmX (RelIncl n),(support b))) /. $1),((b * (SgmX (RelIncl n),(support b))) /. $1);
A1: for k being Element of NAT st k in Seg (len (SgmX (RelIncl n),(support b))) holds
ex x being Element of L st S₁[k,x] ;
consider p being FinSequence of the carrier of L such that
A2: ( dom p = Seg (len (SgmX (RelIncl n),(support b))) & ( for k being Element of NAT st k in Seg (len (SgmX (RelIncl n),(support b))) holds
S₁[k,p /. k] ) ) from POLYNOM2:sch 1(A1);
take Product p ; :: thesis: ex y being FinSequence of the carrier of L st
( len y = len (SgmX (RelIncl n),(support b)) & Product p = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (power L) . ((x * (SgmX (RelIncl n),(support b))) /. i),((b * (SgmX (RelIncl n),(support b))) /. i) ) )
A3: len p = len (SgmX (RelIncl n),(support b)) by A2, FINSEQ_1:def 3;

now

let m be Element of NAT ; :: thesis: ( 1 <= m & m <= len p implies p /. m = (power L) . ((x * (SgmX (RelIncl n),(support b))) /. m),((b * (SgmX (RelIncl n),(support b))) /. m) )
assume ( 1 <= m & m <= len p ) ; :: thesis: p /. m = (power L) . ((x * (SgmX (RelIncl n),(support b))) /. m),((b * (SgmX (RelIncl n),(support b))) /. m)
then m in Seg (len (SgmX (RelIncl n),(support b))) by A3, FINSEQ_1:3;
hence p /. m = (power L) . ((x * (SgmX (RelIncl n),(support b))) /. m),((b * (SgmX (RelIncl n),(support b))) /. m) by A2; :: thesis: verum

end;

hence ex y being FinSequence of the carrier of L st
( len y = len (SgmX (RelIncl n),(support b)) & Product p = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (power L) . ((x * (SgmX (RelIncl n),(support b))) /. i),((b * (SgmX (RelIncl n),(support b))) /. i) ) ) by A3; :: thesis: verum