let n be Ordinal; :: thesis: for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds (1_ (n,L)) *' p = p
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Series of n,L holds (1_ (n,L)) *' p = p
let p be Series of n,L; :: thesis: (1_ (n,L)) *' p = p
set O = 1_ (n,L);
set cL = the carrier of L;

now :: thesis: for b being Element of Bags n holds ((1_ (n,L)) *' p) . b = p . b

let b be Element of Bags n; :: thesis: ((1_ (n,L)) *' p) . b = p . b
consider s being FinSequence of the carrier of L such that
A1: ((1_ (n,L)) *' p) . b = Sum s and
A2: len s = len (decomp b) and
A3: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = ((1_ (n,L)) . b1) * (p . b2) ) by Def10;
not s is empty by A2;
then consider s1 being Element of the carrier of L, t being FinSequence of the carrier of L such that
A4: s1 = s . 1 and
A5: s = <*s1*> ^ t by FINSEQ_3:102;
A6: Sum s = (Sum <*s1*>) + (Sum t) by A5, RLVECT_1:41;

A7: now :: thesis: Sum t = 0. L

per cases ( t = <*> the carrier of L or t <> <*> the carrier of L ) ;

suppose t = <*> the carrier of L ; :: thesis: Sum t = 0. L

hence Sum t = 0. L by RLVECT_1:43; :: thesis: verum

end;

suppose A8: t <> <*> the carrier of L ; :: thesis: Sum t = 0. L

now :: thesis: for k being Nat st k in dom t holds
t /. k = 0. L

let k be Nat; :: thesis: ( k in dom t implies t /. b₁ = 0. L )
A9: len s = (len t) + (len <*s1*>) by A5, FINSEQ_1:22
.= (len t) + 1 by FINSEQ_1:39 ;
assume A10: k in dom t ; :: thesis: t /. b₁ = 0. L
then A11: t /. k = t . k by PARTFUN1:def 6
.= s . (k + 1) by A5, A10, FINSEQ_3:103 ;
1 <= k by A10, FINSEQ_3:25;
then A12: 1 < k + 1 by NAT_1:13;
k <= len t by A10, FINSEQ_3:25;
then A13: k + 1 <= len s by A9, XREAL_1:6;
then A14: k + 1 in dom (decomp b) by A2, A12, FINSEQ_3:25;
A15: dom s = dom (decomp b) by A2, FINSEQ_3:29;
then A16: s /. (k + 1) = s . (k + 1) by A14, PARTFUN1:def 6;

per cases ( k + 1 < len s or k + 1 = len s ) by A13, XXREAL_0:1;

suppose A17: k + 1 < len s ; :: thesis: t /. b₁ = 0. L

consider b1, b2 being bag of n such that
A18: (decomp b) /. (k + 1) = <*b1,b2*> and
A19: s /. (k + 1) = ((1_ (n,L)) . b1) * (p . b2) by A3, A15, A14;
b1 <> EmptyBag n by A2, A12, A17, A18, PRE_POLY:72;
hence t /. k = (0. L) * (p . b2) by A11, A16, A19, Th25
.= 0. L ;
:: thesis: verum

end;

suppose A20: k + 1 = len s ; :: thesis: t /. b₁ = 0. L

A21: now :: thesis: not b = EmptyBag n

assume b = EmptyBag n ; :: thesis: contradiction
then decomp b = <*<*(EmptyBag n),(EmptyBag n)*>*> by PRE_POLY:73;
then (len t) + 1 = 0 + 1 by A2, A9, FINSEQ_1:39;
hence contradiction by A8; :: thesis: verum

end;

consider b1, b2 being bag of n such that
A22: (decomp b) /. (k + 1) = <*b1,b2*> and
A23: s /. (k + 1) = ((1_ (n,L)) . b1) * (p . b2) by A3, A15, A14;
(decomp b) /. (len s) = <*b,(EmptyBag n)*> by A2, PRE_POLY:71;
then ( b2 = EmptyBag n & b1 = b ) by A20, A22, FINSEQ_1:77;
then s . (k + 1) = (0. L) * (p . (EmptyBag n)) by A16, A23, A21, Th25
.= 0. L ;
hence t /. k = 0. L by A11; :: thesis: verum

end;

end;

end;

hence Sum t = 0. L by MATRLIN:11; :: thesis: verum

end;

end;

end;

A24: not s is empty by A2;
then consider b1, b2 being bag of n such that
A25: (decomp b) /. 1 = <*b1,b2*> and
A26: s /. 1 = ((1_ (n,L)) . b1) * (p . b2) by A3, FINSEQ_5:6;
1 in dom s by A24, FINSEQ_5:6;
then A27: s /. 1 = s . 1 by PARTFUN1:def 6;
(decomp b) /. 1 = <*(EmptyBag n),b*> by PRE_POLY:71;
then A28: ( b2 = b & b1 = EmptyBag n ) by A25, FINSEQ_1:77;
Sum <*s1*> = s1 by RLVECT_1:44
.= (1. L) * (p . b) by A4, A26, A28, A27, Th25
.= p . b ;
hence ((1_ (n,L)) *' p) . b = p . b by A1, A6, A7, RLVECT_1:4; :: thesis: verum

end;

hence (1_ (n,L)) *' p = p ; :: thesis: verum