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]

proof

let k be Element of NAT ; :: thesis: ( k in Seg (len (SgmX ((RelIncl n),(support b)))) implies ex x being Element of L st S₁[k,x] )
assume k in Seg (len (SgmX ((RelIncl n),(support b)))) ; :: thesis: ex x being Element of L st S₁[k,x]
then A2: k in dom (SgmX ((RelIncl n),(support b))) by FINSEQ_1:def 3;
take (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. k),((b * (SgmX ((RelIncl n),(support b)))) /. k)) ; :: thesis: ( (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. k),((b * (SgmX ((RelIncl n),(support b)))) /. k)) is Element of L & S₁[k,(power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. k),((b * (SgmX ((RelIncl n),(support b)))) /. k))] )
dom b = n by PARTFUN1:def 2;
then rng (SgmX ((RelIncl n),(support b))) c= dom b by FINSEQ_1:def 4;
then dom (b * (SgmX ((RelIncl n),(support b)))) = dom (SgmX ((RelIncl n),(support b))) by RELAT_1:27;
then (b * (SgmX ((RelIncl n),(support b)))) /. k = (b * (SgmX ((RelIncl n),(support b)))) . k by A2, PARTFUN1:def 6;
hence ( (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. k),((b * (SgmX ((RelIncl n),(support b)))) /. k)) is Element of L & S₁[k,(power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. k),((b * (SgmX ((RelIncl n),(support b)))) /. k))] ) by BINOP_1:17; :: thesis: verum

end;

consider p being FinSequence of the carrier of L such that
A3: ( 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 RECDEF_1:sch 17(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)) ) )
A4: len p = len (SgmX ((RelIncl n),(support b))) by A3, FINSEQ_1:def 3;

now :: thesis: for m being Element of NAT st 1 <= m & m <= len p holds
p /. m = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. m),((b * (SgmX ((RelIncl n),(support b)))) /. m))

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 A4, FINSEQ_1:1;
hence p /. m = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. m),((b * (SgmX ((RelIncl n),(support b)))) /. m)) by A3; :: 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 A4; :: thesis: verum