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

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

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 by A5, A15, FINSEQ_1:def 7 ;
A17: 1 <= k by A15, FINSEQ_3:27;
A18: dom s = dom (decomp b) by A2, FINSEQ_3:31;
A19: len s = (len t) + (len <*s1*>) by A5, FINSEQ_1:35
.= (len t) + 1 by FINSEQ_1:56 ;
k <= len t by A15, FINSEQ_3:27;
then A20: k < len s by A19, NAT_1:13;
then A21: k in dom (decomp b) by A2, A17, FINSEQ_3:27;
then A22: s /. k = s . k by A18, PARTFUN1:def 8;

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

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

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

end;

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

consider b1, b2 being bag of such that
A27: (decomp b) /. k = <*b1,b2*> and
A28: s /. k = (p . b1) * ((1_ n,L) . b2) by A3, A18, A21;
(decomp b) /. 1 = <*(EmptyBag n),b*> by Th75;
then A29: ( b1 = EmptyBag n & b2 = 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 = (p . (EmptyBag n)) * (0. L) by A22, A28, A29, Th84
.= 0. L by VECTSP_1:36 ;
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 (p *' (1_ n,L)) . b = p . b by A1, A6, A13, RLVECT_1:10; :: thesis: verum

end;

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