set S = SgmX ((RelIncl n),(support b));
let a, c be Element of L; :: thesis: ( ex y being FinSequence of the carrier of L st
( len y = len (SgmX ((RelIncl n),(support b))) & a = 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)) ) ) & ex y being FinSequence of the carrier of L st
( len y = len (SgmX ((RelIncl n),(support b))) & c = 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)) ) ) implies a = c )
assume that
A5: ex y1 being FinSequence of the carrier of L st
( len y1 = len (SgmX ((RelIncl n),(support b))) & a = Product y1 & ( for i being Element of NAT st 1 <= i & i <= len y1 holds
y1 /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) ) ) and
A6: ex y2 being FinSequence of the carrier of L st
( len y2 = len (SgmX ((RelIncl n),(support b))) & c = Product y2 & ( for i being Element of NAT st 1 <= i & i <= len y2 holds
y2 /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) ) ) ; :: thesis: a = c
consider y1 being FinSequence of the carrier of L such that
A7: len y1 = len (SgmX ((RelIncl n),(support b))) and
A8: Product y1 = a and
A9: for i being Element of NAT st 1 <= i & i <= len y1 holds
y1 /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) by A5;
consider y2 being FinSequence of the carrier of L such that
A10: len y2 = len (SgmX ((RelIncl n),(support b))) and
A11: Product y2 = c and
A12: for i being Element of NAT st 1 <= i & i <= len y2 holds
y2 /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) by A6;

now :: thesis: for i being Nat st 1 <= i & i <= len y1 holds
y1 . i = y2 . i

let i be Nat; :: thesis: ( 1 <= i & i <= len y1 implies y1 . i = y2 . i )
assume that
A13: 1 <= i and
A14: i <= len y1 ; :: thesis: y1 . i = y2 . i
i in Seg (len y2) by A7, A10, A13, A14, FINSEQ_1:1;
then A15: i in dom y2 by FINSEQ_1:def 3;
A16: i in Seg (len y1) by A13, A14, FINSEQ_1:1;
then i in dom y1 by FINSEQ_1:def 3;
hence y1 . i = y1 /. i by PARTFUN1:def 6
.= (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) by A9, A13, A14, A16
.= y2 /. i by A7, A10, A12, A13, A14, A16
.= y2 . i by A15, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence a = c by A7, A8, A10, A11, FINSEQ_1:14; :: thesis: verum