let n be Ordinal; for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for x being Function of n,L holds eval ((1_ (n,L)),x) = 1. L
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; for x being Function of n,L holds eval ((1_ (n,L)),x) = 1. L
let x be Function of n,L; eval ((1_ (n,L)),x) = 1. L
set 1p = 1_ (n,L);
A1:
for u being object st u in {(EmptyBag n)} holds
u in Support (1_ (n,L))
reconsider s1p = Support (1_ (n,L)) as finite Subset of (Bags n) ;
set sg1p = SgmX ((BagOrder n),s1p);
A4:
BagOrder n linearly_orders Support (1_ (n,L))
by Th10;
for u being object st u in Support (1_ (n,L)) holds
u in {(EmptyBag n)}
then A6:
Support (1_ (n,L)) = {(EmptyBag n)}
by A1, TARSKI:2;
then A7:
rng (SgmX ((BagOrder n),s1p)) = {(EmptyBag n)}
by A4, PRE_POLY:def 2;
then A8:
EmptyBag n in rng (SgmX ((BagOrder n),s1p))
by TARSKI:def 1;
then A9:
1 in dom (SgmX ((BagOrder n),s1p))
by FINSEQ_3:31;
then
(SgmX ((BagOrder n),s1p)) /. 1 = (SgmX ((BagOrder n),s1p)) . 1
by PARTFUN1:def 6;
then
(SgmX ((BagOrder n),s1p)) /. 1 in rng (SgmX ((BagOrder n),s1p))
by A9, FUNCT_1:def 3;
then A10:
(SgmX ((BagOrder n),s1p)) /. 1 = EmptyBag n
by A7, TARSKI:def 1;
A11:
for u being object st u in dom (SgmX ((BagOrder n),s1p)) holds
u in {1}
proof
let u be
object ;
( u in dom (SgmX ((BagOrder n),s1p)) implies u in {1} )
assume A12:
u in dom (SgmX ((BagOrder n),s1p))
;
u in {1}
assume A13:
not
u in {1}
;
contradiction
reconsider u =
u as
Element of
NAT by A12;
(SgmX ((BagOrder n),s1p)) /. u = (SgmX ((BagOrder n),s1p)) . u
by A12, PARTFUN1:def 6;
then A14:
(SgmX ((BagOrder n),s1p)) /. u in rng (SgmX ((BagOrder n),s1p))
by A12, FUNCT_1:def 3;
A15:
u <> 1
by A13, TARSKI:def 1;
A16:
1
< u
(SgmX ((BagOrder n),s1p)) /. 1
= (SgmX ((BagOrder n),s1p)) . 1
by A8, A12, FINSEQ_3:31, PARTFUN1:def 6;
then
(SgmX ((BagOrder n),s1p)) /. 1
in rng (SgmX ((BagOrder n),s1p))
by A9, FUNCT_1:def 3;
then (SgmX ((BagOrder n),s1p)) /. 1 =
EmptyBag n
by A7, TARSKI:def 1
.=
(SgmX ((BagOrder n),s1p)) /. u
by A7, A14, TARSKI:def 1
;
hence
contradiction
by A4, A9, A12, A16, PRE_POLY:def 2;
verum
end;
A18:
dom (1_ (n,L)) = Bags n
by FUNCT_2:def 1;
A19:
1 in dom (SgmX ((BagOrder n),s1p))
by A8, FINSEQ_3:31;
A20:
(SgmX ((BagOrder n),s1p)) . 1 in rng (SgmX ((BagOrder n),s1p))
by A9, FUNCT_1:def 3;
then
(SgmX ((BagOrder n),s1p)) . 1 in {(EmptyBag n)}
by A6, A4, PRE_POLY:def 2;
then
(SgmX ((BagOrder n),s1p)) . 1 = EmptyBag n
by TARSKI:def 1;
then
1 in dom ((1_ (n,L)) * (SgmX ((BagOrder n),s1p)))
by A19, A18, FUNCT_1:11;
then A21: ((1_ (n,L)) * (SgmX ((BagOrder n),s1p))) /. 1 =
((1_ (n,L)) * (SgmX ((BagOrder n),s1p))) . 1
by PARTFUN1:def 6
.=
(1_ (n,L)) . ((SgmX ((BagOrder n),s1p)) . 1)
by A9, FUNCT_1:13
.=
(1_ (n,L)) . (EmptyBag n)
by A7, A20, TARSKI:def 1
.=
1. L
by POLYNOM1:25
;
consider y being FinSequence of the carrier of L such that
A22:
len y = len (SgmX ((BagOrder n),s1p))
and
A23:
Sum y = eval ((1_ (n,L)),x)
and
A24:
for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (((1_ (n,L)) * (SgmX ((BagOrder n),s1p))) /. i) * (eval (((SgmX ((BagOrder n),s1p)) /. i),x))
by Def2;
for u being object st u in {1} holds
u in dom (SgmX ((BagOrder n),s1p))
by A9, TARSKI:def 1;
then
dom (SgmX ((BagOrder n),s1p)) = Seg 1
by A11, FINSEQ_1:2, TARSKI:2;
then A25:
len (SgmX ((BagOrder n),s1p)) = 1
by FINSEQ_1:def 3;
then y . 1 =
y /. 1
by A22, FINSEQ_4:15
.=
(((1_ (n,L)) * (SgmX ((BagOrder n),s1p))) /. 1) * (eval (((SgmX ((BagOrder n),s1p)) /. 1),x))
by A25, A22, A24
.=
(((1_ (n,L)) * (SgmX ((BagOrder n),s1p))) /. 1) * (1. L)
by A10, Th6
.=
((1_ (n,L)) * (SgmX ((BagOrder n),s1p))) /. 1
;
then
y = <*(1. L)*>
by A25, A22, A21, FINSEQ_1:40;
hence
eval ((1_ (n,L)),x) = 1. L
by A23, RLVECT_1:44; verum