let n be Ordinal; for L being 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 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 3;
then reconsider xu = x . u as Element of L by A3;
A5:
RelIncl n linearly_orders sb
by PRE_POLY:82;
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:31;
then A9:
(SgmX ((RelIncl n),sb)) . 1 in rng (SgmX ((RelIncl n),sb))
by FUNCT_1:def 3;
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:11;
then A11: (x * (SgmX ((RelIncl n),sb))) /. 1 =
(x * (SgmX ((RelIncl n),sb))) . 1
by PARTFUN1:def 6
.=
x . ((SgmX ((RelIncl n),sb)) . 1)
by A8, FUNCT_1:13
.=
x . u
by A6, A9, TARSKI:def 1
;
dom b = n
by PARTFUN1:def 2;
then
1 in dom (b * (SgmX ((RelIncl n),sb)))
by A8, A10, A2, FUNCT_1:11;
then A12: (b * (SgmX ((RelIncl n),sb))) /. 1 =
(b * (SgmX ((RelIncl n),sb))) . 1
by PARTFUN1:def 6
.=
b . ((SgmX ((RelIncl n),sb)) . 1)
by A8, FUNCT_1:13
.=
b . u
by A6, A9, TARSKI:def 1
;
A13:
(power L) . (xu,(b . u)) = (power L) . [xu,(b . u)]
;
A14:
for v being object st v in dom (SgmX ((RelIncl n),sb)) holds
v in {1}
proof
let v be
object ;
( 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 6;
then A17:
(SgmX ((RelIncl n),sb)) /. v in rng (SgmX ((RelIncl n),sb))
by A15, FUNCT_1:def 3;
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:31, PARTFUN1:def 6;
then
(SgmX ((RelIncl n),sb)) /. 1
in rng (SgmX ((RelIncl n),sb))
by A8, FUNCT_1:def 3;
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 Def1;
for v being object 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:2, TARSKI:2;
then A24:
len (SgmX ((RelIncl n),sb)) = 1
by FINSEQ_1:def 3;
then y . 1 =
y /. 1
by A21, FINSEQ_4:15
.=
(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:40;
hence
eval (b,x) = (power L) . ((x . u),(b . u))
by A22, A13, GROUP_4:9; verum