let n be Ordinal; for L being non empty non trivial well-unital doubleLoopStr
for u being set
for b being bag of n st support b = {u} holds
for x being Function of n,L holds eval b,x = (power L) . (x . u),(b . u)
let L be non empty non trivial well-unital doubleLoopStr ; for u being set
for b being bag of n st support b = {u} holds
for x being Function of n,L holds eval b,x = (power L) . (x . u),(b . u)
let u be set ; for b being bag of n st support b = {u} holds
for x being Function of n,L holds eval b,x = (power L) . (x . u),(b . u)
let b be bag of n; ( support b = {u} implies for x being Function of n,L holds eval b,x = (power L) . (x . u),(b . u) )
reconsider sb = support b as finite Subset of n ;
set sg = SgmX (RelIncl n),sb;
assume A1:
support b = {u}
; for x being Function of n,L holds eval b,x = (power L) . (x . u),(b . u)
then A2:
u in support b
by TARSKI:def 1;
let x be Function of n,L; eval b,x = (power L) . (x . u),(b . u)
A3:
rng x c= the carrier of L
by RELAT_1:def 19;
A4:
n = dom x
by FUNCT_2:def 1;
then
x . u in rng x
by A2, FUNCT_1:def 5;
then reconsider xu = x . u as Element of L by A3;
A5:
RelIncl n linearly_orders sb
by Th15;
then A6:
rng (SgmX (RelIncl n),sb) = {u}
by A1, PRE_POLY:def 2;
then A7:
u in rng (SgmX (RelIncl n),sb)
by TARSKI:def 1;
then A8:
1 in dom (SgmX (RelIncl n),sb)
by FINSEQ_3:33;
then A9:
(SgmX (RelIncl n),sb) . 1 in rng (SgmX (RelIncl n),sb)
by FUNCT_1:def 5;
then A10:
(SgmX (RelIncl n),sb) . 1 = u
by A6, TARSKI:def 1;
then
1 in dom (x * (SgmX (RelIncl n),sb))
by A4, A8, A2, FUNCT_1:21;
then A11: (x * (SgmX (RelIncl n),sb)) /. 1 =
(x * (SgmX (RelIncl n),sb)) . 1
by PARTFUN1:def 8
.=
x . ((SgmX (RelIncl n),sb) . 1)
by A8, FUNCT_1:23
.=
x . u
by A6, A9, TARSKI:def 1
;
dom b = n
by PARTFUN1:def 4;
then
1 in dom (b * (SgmX (RelIncl n),sb))
by A8, A10, A2, FUNCT_1:21;
then A12: (b * (SgmX (RelIncl n),sb)) /. 1 =
(b * (SgmX (RelIncl n),sb)) . 1
by PARTFUN1:def 8
.=
b . ((SgmX (RelIncl n),sb) . 1)
by A8, FUNCT_1:23
.=
b . u
by A6, A9, TARSKI:def 1
;
A13:
(power L) . xu,(b . u) = (power L) . [xu,(b . u)]
;
A14:
for v being set st v in dom (SgmX (RelIncl n),sb) holds
v in {1}
proof
let v be
set ;
( v in dom (SgmX (RelIncl n),sb) implies v in {1} )
assume A15:
v in dom (SgmX (RelIncl n),sb)
;
v in {1}
assume A16:
not
v in {1}
;
contradiction
reconsider v =
v as
Element of
NAT by A15;
(SgmX (RelIncl n),sb) /. v = (SgmX (RelIncl n),sb) . v
by A15, PARTFUN1:def 8;
then A17:
(SgmX (RelIncl n),sb) /. v in rng (SgmX (RelIncl n),sb)
by A15, FUNCT_1:def 5;
A18:
v <> 1
by A16, TARSKI:def 1;
A19:
1
< v
(SgmX (RelIncl n),sb) /. 1
= (SgmX (RelIncl n),sb) . 1
by A7, A15, FINSEQ_3:33, PARTFUN1:def 8;
then
(SgmX (RelIncl n),sb) /. 1
in rng (SgmX (RelIncl n),sb)
by A8, FUNCT_1:def 5;
then (SgmX (RelIncl n),sb) /. 1 =
u
by A6, TARSKI:def 1
.=
(SgmX (RelIncl n),sb) /. v
by A6, A17, TARSKI:def 1
;
hence
contradiction
by A5, A8, A15, A19, PRE_POLY:def 2;
verum
end;
consider y being FinSequence of the carrier of L such that
A21:
len y = len (SgmX (RelIncl n),(support b))
and
A22:
eval b,x = Product y
and
A23:
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 Def2;
for v being set st v in {1} holds
v in dom (SgmX (RelIncl n),sb)
by A8, TARSKI:def 1;
then
dom (SgmX (RelIncl n),sb) = Seg 1
by A14, FINSEQ_1:4, TARSKI:2;
then A24:
len (SgmX (RelIncl n),sb) = 1
by FINSEQ_1:def 3;
then y . 1 =
y /. 1
by A21, FINSEQ_4:24
.=
(power L) . ((x * (SgmX (RelIncl n),sb)) /. 1),((b * (SgmX (RelIncl n),sb)) /. 1)
by A21, A23, A24
;
then
y = <*((power L) . (x . u),(b . u))*>
by A21, A24, A12, A11, FINSEQ_1:57;
hence
eval b,x = (power L) . (x . u),(b . u)
by A22, A13, GROUP_4:12; verum