let n be Ordinal; :: thesis: for L being non empty 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 empty non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for x being Function of n,L holds eval (1_ n,L),x = 1. L
let x be Function of n,L; :: thesis: eval (1_ n,L),x = 1. L
set 1p = 1_ n,L;
A1: for u being set st u in Support (1_ n,L) holds
u in {(EmptyBag n)}

proof

let u be set ; :: thesis: ( u in Support (1_ n,L) implies u in {(EmptyBag n)} )
assume A2: u in Support (1_ n,L) ; :: thesis: u in {(EmptyBag n)}
then reconsider u = u as Element of Bags n ;
(1_ n,L) . u <> 0. L by A2, POLYNOM1:def 9;
then u = EmptyBag n by POLYNOM1:84;
hence u in {(EmptyBag n)} by TARSKI:def 1; :: thesis: verum

end;

for u being set st u in {(EmptyBag n)} holds
u in Support (1_ n,L)

proof

let u be set ; :: thesis: ( u in {(EmptyBag n)} implies u in Support (1_ n,L) )
assume A3: u in {(EmptyBag n)} ; :: thesis: u in Support (1_ n,L)
then A4: u = EmptyBag n by TARSKI:def 1;
reconsider u = u as Element of Bags n by A3, TARSKI:def 1;
(1_ n,L) . u = 1. L by A4, POLYNOM1:84;
then (1_ n,L) . u <> 0. L by POLYNOM1:27;
hence u in Support (1_ n,L) by POLYNOM1:def 9; :: thesis: verum

end;

then A5: Support (1_ n,L) = {(EmptyBag n)} by A1, TARSKI:2;
reconsider s1p = Support (1_ n,L) as finite Subset of (Bags n) ;
set sg1p = SgmX (BagOrder n),s1p;
A6: BagOrder n linearly_orders Support (1_ n,L) by Th20;
then A7: ( rng (SgmX (BagOrder n),s1p) = {(EmptyBag n)} & ( for l, m being Element of NAT st l in dom (SgmX (BagOrder n),s1p) & m in dom (SgmX (BagOrder n),s1p) & l < m holds
( (SgmX (BagOrder n),s1p) /. l <> (SgmX (BagOrder n),s1p) /. m & [((SgmX (BagOrder n),s1p) /. l),((SgmX (BagOrder n),s1p) /. m)] in BagOrder n ) ) ) by A5, TRIANG_1: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:33;
then A10: for u being set st u in {1} holds
u in dom (SgmX (BagOrder n),s1p) by TARSKI:def 1;
for u being set st u in dom (SgmX (BagOrder n),s1p) holds
u in {1}

proof

let u be set ; :: thesis: ( u in dom (SgmX (BagOrder n),s1p) implies u in {1} )
assume A11: u in dom (SgmX (BagOrder n),s1p) ; :: thesis: u in {1}
assume A12: not u in {1} ; :: thesis: contradiction
reconsider u = u as Element of NAT by A11;
A13: u <> 1 by A12, TARSKI:def 1;
A14: 1 < u

proof

consider k being Nat such that
A15: dom (SgmX (BagOrder n),s1p) = Seg k by FINSEQ_1:def 2;
Seg k = { m where m is Element of NAT : ( 1 <= m & m <= k ) } by FINSEQ_1:def 1;
then consider m' being Element of NAT such that
A16: ( m' = u & 1 <= m' & m' <= k ) by A11, A15;
thus 1 < u by A13, A16, XXREAL_0:1; :: thesis: verum

end;

( (SgmX (BagOrder n),s1p) /. 1 = (SgmX (BagOrder n),s1p) . 1 & (SgmX (BagOrder n),s1p) /. u = (SgmX (BagOrder n),s1p) . u ) by A8, A11, FINSEQ_3:33, PARTFUN1:def 8;
then A17: ( (SgmX (BagOrder n),s1p) /. 1 in rng (SgmX (BagOrder n),s1p) & (SgmX (BagOrder n),s1p) /. u in rng (SgmX (BagOrder n),s1p) ) by A9, A11, FUNCT_1:def 5;
then (SgmX (BagOrder n),s1p) /. 1 = EmptyBag n by A7, TARSKI:def 1
.= (SgmX (BagOrder n),s1p) /. u by A7, A17, TARSKI:def 1 ;
hence contradiction by A6, A9, A11, A14, TRIANG_1:def 2; :: thesis: verum

end;

then dom (SgmX (BagOrder n),s1p) = Seg 1 by A10, FINSEQ_1:4, TARSKI:2;
then A18: len (SgmX (BagOrder n),s1p) = 1 by FINSEQ_1:def 3;
(SgmX (BagOrder n),s1p) /. 1 = (SgmX (BagOrder n),s1p) . 1 by A9, PARTFUN1:def 8;
then (SgmX (BagOrder n),s1p) /. 1 in rng (SgmX (BagOrder n),s1p) by A9, FUNCT_1:def 5;
then A19: (SgmX (BagOrder n),s1p) /. 1 = EmptyBag n by A7, TARSKI:def 1;
consider y being FinSequence of the carrier of L such that
A20: ( len y = len (SgmX (BagOrder n),s1p) & Sum y = eval (1_ n,L),x & ( 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 Def4;
A21: y . 1 = y /. 1 by A18, A20, FINSEQ_4:24
.= (((1_ n,L) * (SgmX (BagOrder n),s1p)) /. 1) * (eval (((SgmX (BagOrder n),s1p) /. 1) @ ),x) by A18, A20
.= (((1_ n,L) * (SgmX (BagOrder n),s1p)) /. 1) * (1. L) by A19, Th16
.= ((1_ n,L) * (SgmX (BagOrder n),s1p)) /. 1 by VECTSP_1:def 16 ;
A22: (SgmX (BagOrder n),s1p) . 1 in rng (SgmX (BagOrder n),s1p) by A9, FUNCT_1:def 5;
A23: 1 in dom (SgmX (BagOrder n),s1p) by A8, FINSEQ_3:33;
(SgmX (BagOrder n),s1p) . 1 in {(EmptyBag n)} by A5, A6, A22, TRIANG_1:def 2;
then A24: (SgmX (BagOrder n),s1p) . 1 = EmptyBag n by TARSKI:def 1;
dom (1_ n,L) = Bags n by FUNCT_2:def 1;
then 1 in dom ((1_ n,L) * (SgmX (BagOrder n),s1p)) by A23, A24, FUNCT_1:21;
then ((1_ n,L) * (SgmX (BagOrder n),s1p)) /. 1 = ((1_ n,L) * (SgmX (BagOrder n),s1p)) . 1 by PARTFUN1:def 8
.= (1_ n,L) . ((SgmX (BagOrder n),s1p) . 1) by A9, FUNCT_1:23
.= (1_ n,L) . (EmptyBag n) by A7, A22, TARSKI:def 1
.= 1. L by POLYNOM1:84 ;
then y = <*(1. L)*> by A18, A20, A21, FINSEQ_1:57;
hence eval (1_ n,L),x = 1. L by A20, RLVECT_1:61; :: thesis: verum