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 empty 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

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 st
( (decomp b) /. k = <*b1,b2*> & s /. k = ((1_ n,L) . b1) * (p . b2) ) by Def26;
A4: len s <> 0 by A2;
then not s is empty ;
then consider s1 being Element of the carrier of L, t being FinSequence of the carrier of L such that
A5: s1 = s . 1 and
A6: s = <*s1*> ^ t by FINSEQ_3:111;
A7: Sum s = (Sum <*s1*>) + (Sum t) by A6, RLVECT_1:58;
not s is empty by A4;
then A8: 1 in dom s by FINSEQ_5:6;
then consider b1, b2 being bag of such that
A9: (decomp b) /. 1 = <*b1,b2*> and
A10: s /. 1 = ((1_ n,L) . b1) * (p . b2) by A3;
(decomp b) /. 1 = <*(EmptyBag n),b*> by Th75;
then A11: ( b2 = b & b1 = EmptyBag n ) by A9, GROUP_7:2;
A12: s /. 1 = s . 1 by A8, PARTFUN1:def 8;
A13: Sum <*s1*> = s1 by RLVECT_1:61
.= (1. L) * (p . b) by A5, A10, A11, A12, Th84
.= p . b by VECTSP_1:def 16 ;

now

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:60; :: thesis: verum

end;

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

now

let k be Nat; :: thesis: ( k in dom t implies t /. b₁ = 0. L )
assume A15: k in dom t ; :: thesis: t /. b₁ = 0. L
then A16: t /. k = t . k by PARTFUN1:def 8
.= s . (k + 1) by A6, A15, FINSEQ_3:112 ;
1 <= k by A15, FINSEQ_3:27;
then A17: 1 < k + 1 by NAT_1:13;
A18: dom s = dom (decomp b) by A2, FINSEQ_3:31;
A19: len s = (len t) + (len <*s1*>) by A6, FINSEQ_1:35
.= (len t) + 1 by FINSEQ_1:56 ;
k <= len t by A15, FINSEQ_3:27;
then A20: k + 1 <= len s by A19, XREAL_1:8;
then A21: k + 1 in dom (decomp b) by A2, A17, FINSEQ_3:27;
then A22: s /. (k + 1) = s . (k + 1) by A18, PARTFUN1:def 8;

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

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

consider b1, b2 being bag of such that
A24: (decomp b) /. (k + 1) = <*b1,b2*> and
A25: s /. (k + 1) = ((1_ n,L) . b1) * (p . b2) by A3, A18, A21;
b1 <> EmptyBag n by A2, A17, A23, A24, Th76;
hence t /. k = (0. L) * (p . b2) by A16, A22, A25, Th84
.= 0. L by VECTSP_1:39 ;
:: thesis: verum

end;

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

consider b1, b2 being bag of such that
A27: (decomp b) /. (k + 1) = <*b1,b2*> and
A28: s /. (k + 1) = ((1_ n,L) . b1) * (p . b2) by A3, A18, A21;
(decomp b) /. (len s) = <*b,(EmptyBag n)*> by A2, Th75;
then A29: ( b2 = EmptyBag n & b1 = b ) by A26, A27, GROUP_7:2;

now

assume b = EmptyBag n ; :: thesis: contradiction
then decomp b = <*<*(EmptyBag n),(EmptyBag n)*>*> by Th77;
then (len t) + 1 = 0 + 1 by A2, A19, FINSEQ_1:56;
hence contradiction by A14; :: thesis: verum

end;

then s . (k + 1) = (0. L) * (p . (EmptyBag n)) by A22, A28, A29, Th84
.= 0. L by VECTSP_1:39 ;
hence t /. k = 0. L by A16; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

hence ((1_ n,L) *' p) . b = p . b by A1, A7, A13, RLVECT_1:10; :: thesis: verum

end;

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