set S = SgmX ((RelIncl n),(support b));
let a, c be Element of L; ( 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
A4:
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
A5:
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)) ) )
; a = c
consider y1 being FinSequence of the carrier of L such that
A6:
len y1 = len (SgmX ((RelIncl n),(support b)))
and
A7:
Product y1 = a
and
A8:
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 A4;
consider y2 being FinSequence of the carrier of L such that
A9:
len y2 = len (SgmX ((RelIncl n),(support b)))
and
A10:
Product y2 = c
and
A11:
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 A5;
now for i being Nat st 1 <= i & i <= len y1 holds
y1 . i = y2 . ilet i be
Nat;
( 1 <= i & i <= len y1 implies y1 . i = y2 . i )assume that A12:
1
<= i
and A13:
i <= len y1
;
y1 . i = y2 . i
i in Seg (len y2)
by A6, A9, A12, A13, FINSEQ_1:1;
then A14:
i in dom y2
by FINSEQ_1:def 3;
A15:
i in Seg (len y1)
by A12, A13, 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 A8, A12, A13, A15
.=
y2 /. i
by A6, A9, A11, A12, A13, A15
.=
y2 . i
by A14, PARTFUN1:def 6
;
verum end;
hence
a = c
by A6, A7, A9, A10, FINSEQ_1:14; verum