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

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

let b be Element of Bags n; :: thesis: (p *' (1_ (n,L))) . b = p . b
consider s being FinSequence of the carrier of L such that
A1: (p *' (1_ (n,L))) . 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 = (p . b1) * ((1_ (n,L)) . b2) ) by Def10;
consider t being FinSequence of the carrier of L, s1 being Element of the carrier of L such that
A4: s = t ^ <*s1*> by A2, FINSEQ_2:19;

A5: 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 A6: 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 )
A7: len s = (len t) + (len <*s1*>) by A4, FINSEQ_1:22
.= (len t) + 1 by FINSEQ_1:39 ;
assume A8: k in dom t ; :: thesis: t /. b₁ = 0. L
then A9: t /. k = t . k by PARTFUN1:def 6
.= s . k by A4, A8, FINSEQ_1:def 7 ;
k <= len t by A8, FINSEQ_3:25;
then A10: k < len s by A7, NAT_1:13;
A11: 1 <= k by A8, FINSEQ_3:25;
then A12: k in dom (decomp b) by A2, A10, FINSEQ_3:25;
A13: dom s = dom (decomp b) by A2, FINSEQ_3:29;
then A14: s /. k = s . k by A12, PARTFUN1:def 6;

per cases ( 1 < k or k = 1 ) by A11, XXREAL_0:1;

suppose A15: 1 < k ; :: thesis: t /. b₁ = 0. L

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

end;

suppose A18: k = 1 ; :: thesis: t /. b₁ = 0. L

A19: 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, A7, FINSEQ_1:39;
hence contradiction by A6; :: thesis: verum

end;

consider b1, b2 being bag of n such that
A20: (decomp b) /. k = <*b1,b2*> and
A21: s /. k = (p . b1) * ((1_ (n,L)) . b2) by A3, A13, A12;
(decomp b) /. 1 = <*(EmptyBag n),b*> by PRE_POLY:71;
then ( b1 = EmptyBag n & b2 = b ) by A18, A20, FINSEQ_1:77;
then s . k = (p . (EmptyBag n)) * (0. L) by A14, A21, A19, Th25
.= 0. L ;
hence t /. k = 0. L by A9; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

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